unison/unison-src/errors/io-state1.u

18 lines
409 B
Plaintext

--IO/State1 ability
ability IO where
launchMissiles : {IO} ()
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)
()
()