FoobarE.idr

module FoobarE

import Effects
import Effect.State
import Effect.StdIO

MyProg : Type -> Type
MyProg rTy = Eff rTy ['mystate ::: STATE (List Nat), STDIO]

register : Nat -> MyProg ()
register x = 'mystate :- update (x::)

count : MyProg Nat
count = pure (length !('mystate :- get))


myProg : MyProg ()
myProg = do
  register 1
  register 2
  printLn !count
  register 3
  register 4
  printLn !count


namespace Main
  main : IO ()
  main = run myProg