Idris2Doc : Data.InductionRecursion.DybjerSetzer

Data.InductionRecursion.DybjerSetzer

There are different flavours of induction-recursion. This is the one
introduced in Dybjer and Setzer's paper:
Indexed induction-recursion

data Code : (sort -> Type) -> Type -> Type

Totality: total
Constructors:

Yield : output -> Code input output
Store : (payload : Type) -> (payload -> Code input output) -> Code input output
Branch : (label : Type) -> (toSort : (label -> sort)) -> (((l : label) -> input (toSort l)) -> Code input output) -> Code input output

Decode : Mu f s -> input s

DecodeOutput : (c : Code input output) -> (x : Lazy (sort -> Type)) -> (f : (Force x s -> input s)) -> DecodeType c Force x (\{s:481} => f) -> output

DecodeType : Code input output -> (x : (sort -> Type)) -> (x s -> input s) -> Type

data Mu : ((s : sort) -> Code input (input s)) -> sort -> Type

Totality: not strictly positive
Constructor:

MkMu : DecodeType (f s) (Mu f) (\{s:601} => Decode) -> Mu f s

bind : Code i o -> (o -> Code i o') -> Code i o'