plutus-core-1.0.0.1: Language library for Plutus Core
Safe HaskellNone
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)