PlutusCore.StdLib.Data.ChurchNat
Description
Church-encoded nat and related functions.
nat
churchNat ∷ Type TyName uni () Source #
Church-encoded Nat as a PLC type.
Nat
all (r :: *). r -> (r -> r) -> r
churchZero ∷ TermLike term TyName Name uni fun ⇒ term () Source #
Church-encoded '0' as a PLC term.
/\(r :: *) -> \(z : r) (f : r -> r) -> z
churchSucc ∷ TermLike term TyName Name uni fun ⇒ term () Source #
Church-encoded succ as a PLC term.
succ
\(n : nat) -> /\(r :: *) -> \(z : r) (f : r -> r) -> f (n {r} z f)