Documentation

Fixpoint recursion. Used to encode recursive functions.

Example:

iterateN' ::
 Term s (PInteger :--> (a :--> a) :--> a :--> a) ->
 Term s PInteger ->
 Term s (a :--> a) ->
 Term s a
iterateN' self n f x =
  pif (n #== 0) x (self # n - 1 #$ f x)

iterateN :: Term s (PInteger :--> (a :--> a) :--> a :--> a)
iterateN = pfix #$ plam iterateN'

Further examples can be found in examples/Recursion.hs