Idris2Doc : Control.Linear.LIO

Control.Linear.LIO

(>>) : LinearBindio => (1 _ : Lio ()) -> (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
dataL : (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
interfaceLinearBind : (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
dataUsage : 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_k () b
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