Idris2Doc : Control.Monad.Elin

Control.Monad.Elin

(source)
Reexports
import public Control.Monad.MCancel
import public Data.Linear.ELift1
Definitions
record Elin : Type -> List Type -> Type -> Type
  A monad for running pure, stateful computations in
  state thread `s` with the potential of failing with one
  of the errors listed in `es`.

  Totality: total
  Visibility: public export
  Constructor: 
E : E1 s es a -> Elin s es a

  Projection: 
.run : Elin s es a -> E1 s es a

  Hints:
  
ELift1 s (Elin s)
  
HasIO (Elin World es)
  
MCancel (Elin s)
  
MErr (Elin s)
.run : Elin s es a -> E1 s es a
  Totality: total
  Visibility: public export
run : Elin s es a -> E1 s es a
  Totality: total
  Visibility: public export
runElin : Elin s es a -> Result es a
  When universally quantified over `s`, the `Elin` monad can
  be run to produce a pure value of type `Result es a`, even though
  running the value might involve working with freshly allocated
  mutable state.

  Totality: total
  Visibility: export
runElinIO : Elin World es a -> IO (Result es a)
  When tagged with `World`, the `Elin` monad is just `IO` plus
  error handling.

  Totality: total
  Visibility: export