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

PlutusCore.StdLib.Data.ChurchNat

Description

Church-encoded nat and related functions.

Synopsis

Documentation

churchNatType TyName uni () Source #

Church-encoded Nat as a PLC type.

all (r :: *). r -> (r -> r) -> r

churchZeroTermLike term TyName Name uni fun ⇒ term () Source #

Church-encoded '0' as a PLC term.

/\(r :: *) -> \(z : r) (f : r -> r) -> z

churchSuccTermLike 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)