plutus-core-1.40.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.StdLib.Data.ChurchNat

Description

Church-encoded nat and related functions.

Synopsis

Documentation

churchNat ∷ Type TyName uni () Source #

Church-encoded Nat as a PLC type.

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.

\(n : nat) -> /\(r :: *) -> \(z : r) (f : r -> r) -> f (n {r} z f)