Idris2Doc : Control.Linear.LIO

Control.Linear.LIO

(>>) : LinearBindio => (1 _ : LioUnit) -> (1 _ : Liob) -> Liob

Fixity Declaration: infixl operator, level 1
(>>=) : LinearBindio => (1 _ : Lioa) -> (1 _ : ContTypeiou_actu_kab) -> Liob

Fixity Declaration: infixl operator, level 1
ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
L : (Type -> Type) -> {defaultUnrestricted _ : Usage} -> Type -> Type
A wrapper which allows operations to state the multiplicity of the value
they return. For example, `L IO {use=1} File` is an IO operation which
returns a file that must be used exactly once.
Totality: total
Constructors:
Pure0 : (0 _ : a) -> Lioa
Pure1 : (1 _ : a) -> Lioa
PureW : a -> Lioa
Action : (1 _ : ioa) -> Lioa
Bind : (1 _ : Lioa) -> (1 _ : ContTypeiou_actu_kab) -> Liob
L0 : (Type -> Type) -> Type -> Type
L1 : (Type -> Type) -> Type -> Type
LinearBind : (Type -> Type) -> Type
Like `Monad`, but the action and continuation must be run exactly once
to ensure that the computation is linear.
Parameters: io
Methods:
bindL : (1 _ : ioa) -> (1 _ : (a -> iob)) -> iob

Implementation: 
LinearBindIO
LinearIO : (Type -> Type) -> Type
Usage : Type
Required usage on the result value of a computation
Totality: total
Constructors:
None : Usage
Linear : Usage
Unrestricted : Usage
bindL : LinearBindio => (1 _ : ioa) -> (1 _ : (a -> iob)) -> iob
delay : (1 _ : Liob) -> ContTypeiou_actu_kUnitb
fromInteger : (x : Integer) -> Either (x = 0) (x = 1) => Usage
pure0 : (0 _ : a) -> Lioa
pure1 : (1 _ : a) -> Lioa
run : (Applicativeio, LinearBindio) => (1 _ : Lioa) -> ioa
Run a linear program exactly once, with unrestricted return value in the
underlying context