Data.InductionRecursion.DybjerSetzer(source)

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

Definitions

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

Totality: total
Visibility: public export
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

Hints:

Applicative (Code i)

Functor (Code i)

Monad (Code i)

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

Visibility: public export

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

Visibility: public export

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

Totality: not strictly positive
Visibility: public export
Constructor: 

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

Decode : Mu f s -> input s

Visibility: public export

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

Visibility: public export