unison/unison-src/tests/io-state2.u

17 lines
361 B
Plaintext

--IO/State2 effect
effect IO where
launch-missiles : {IO} ()
effect State se2 where
put : ∀ se . se -> {State se} ()
get : ∀ se . {State se} se
foo : () -> {IO} ()
foo unit =
inc-by : Int64 -> {IO, State Int64} ()
inc-by i =
IO.launch-missiles -- OK, since declared by `inc-by` signature
y = State.get
State.put (y Int64.+ i)
()
()