Idris2Doc : Control.Linear.LIO

Control.Linear.LIO

Definitions

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
bindL : LinearBindio=> (1_ : ioa) -> (1_ : (a->iob)) ->iob
Visibility: public export
dataUsage : Type
  Required usage on the result value of a computation

Totality: total
Visibility: public export
Constructors:
None : Usage
Linear : Usage
Unrestricted : Usage
fromInteger : (x : Integer) ->Either (x=0) (x=1) =>Usage
Visibility: public export
0ContType : (Type->Type) ->Usage->Usage->Type->Type->Type
Visibility: public export
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
Visibility: export
Constructors:
Pure0 : (0_ : a) ->Lioa
Pure1 : (1_ : a) ->Lioa
PureW : a->Lioa
Action : (1_ : ioa) ->Lioa
Bind : (1_ : Lioa) -> (1_ : ContTypeiou_actu_kab) ->Liob

Hints:
Applicativeio=>Applicative (Lio)
Functorio=>Functor (Lio)
(LinearBindio, HasLinearIOio) =>HasLinearIO (Lio)
(Applicativem, LinearBindm) =>Monad (Lm)
L0 : (Type->Type) ->Type->Type
Visibility: public export
L1 : (Type->Type) ->Type->Type
Visibility: public export
run : Applicativeio=>LinearBindio=> (1_ : Lioa) ->ioa
  Run a linear program exactly once, with unrestricted return value in the
underlying context

Visibility: export
(>>=) : LinearBindio=> (1_ : Lioa) -> (1_ : ContTypeiou_actu_kab) ->Liob
Visibility: export
Fixity Declaration: infixl operator, level 1
delay : (1_ : Liob) ->ContTypeiou_actu_k () b
Visibility: export
(>>) : LinearBindio=> (1_ : Lio ()) -> (1_ : Liob) ->Liob
Visibility: export
Fixity Declaration: infixl operator, level 1
pure0 : (0_ : a) ->Lioa
Visibility: export
pure1 : (1_ : a) ->Lioa
Visibility: export
LinearIO : (Type->Type) ->Type
Visibility: public export