--IO/State1 ability

structural ability IO where

launchMissiles : {IO} ()

structural ability State se2 where

put : ∀ se . se -> {State se} ()

get : ∀ se . () -> {State se} se

foo : () -> {IO} ()

foo unit =

-- inner binding can't access outer abilities unless it declares

-- them explicitly

incBy : Int -> {State Int} ()

incBy i =

launchMissiles -- not allowed

y = State.get()

State.put (y Int.+ i)

()

()