Idris2Doc : Data.InductionRecursion.DybjerSetzer

Data.InductionRecursion.DybjerSetzer

Code : (sort -> Type) -> Type -> Type
Totality: total
Constructors:
Yield : output -> Codeinputoutput
Store : (payload : Type) -> (payload -> Codeinputoutput) -> Codeinputoutput
Branch : (label : Type) -> (toSort : (label -> sort)) -> (((l : label) -> input (toSortl)) -> Codeinputoutput) -> Codeinputoutput
Decode : Mufs -> inputs
Totality: total
DecodeOutput : (c : Codeinputoutput) -> (x : Lazy (sort -> Type)) -> (f : (Force xs -> inputs)) -> DecodeTypec Force x (\{s:496} => f) -> output
Totality: total
DecodeType : Codeinputoutput -> (x : (sort -> Type)) -> (xs -> inputs) -> Type
Totality: total
Mu : ((s : sort) -> Codeinput (inputs)) -> sort -> Type
Totality: total
Constructor: 
MkMu : DecodeType (fs) (Muf) (\{s:652} => Decode) -> Mufs
bind : Codeio -> (o -> Codeio') -> Codeio'
Totality: total