Idris2Doc : Data.Recursion.Free


General : (a : Type) -> (a -> Type) -> Type -> Type
Syntax for a program using general recursion
Totality: total
Tell : x -> Generalabx
We can return a value without performing any recursive call.
Ask : (i : a) -> (bi -> Generalabx) -> Generalabx
Or we can pick an input and ask an oracle to give us a return value
for it. The second argument is a continuation explaining what we want
to do with the returned value.
PiG : (a : Type) -> (a -> Type) -> Type
Type of functions using general recursion
Totality: total
already : Generalabx -> Maybex
Check whehther we are ready to return a value
Totality: total
bind : Generalabx -> (x -> Generalaby) -> Generalaby
Monadic bind (defined outside of the interface to be able to use it for
map and (<*>)).
Totality: total
call : PiGab
Perform a recursive call and return the value provided by the oracle.
Totality: total
engine : PiGab -> Nat -> Generalabx -> Generalabx
Recursively call expand a set number of times.
Totality: total
expand : PiGab -> Generalabx -> Generalabx
Use a function using general recursion to expand all of the oracle calls.
Totality: total
fold : (x -> y) -> ((i : a) -> (bi -> y) -> y) -> Generalabx -> y
Recursor for General
Totality: total
late : PiGab -> Generalabx -> Latex
Rely on an oracle using general recursion to convert a function using
general recursion into a process returning a value in the (distant) future.
Totality: total
lazy : PiGab -> (i : a) -> Late (bi)
Interpret a function using general recursion as a process returning
a value in the (distant) future.
Totality: total
monadMorphism : Monadm => ((i : a) -> m (bi)) -> Generalabx -> mx
Given a monadic oracle we can give a monad morphism interpreting a
function using general recursion as a monadic process.
Totality: total
petrol : PiGab -> Nat -> (i : a) -> Maybe (bi)
Check whether recursively calling expand a set number of times is enough
to produce a value.
Totality: total