Safe Haskell	None
Language	Haskell2010

PlutusCore.StdLib.Data.ChurchNat

Description

Church-encoded nat and related functions.

Synopsis

churchNat :: forall (uni :: Type -> Type). Type TyName uni ()
churchZero :: forall term (uni :: Type -> Type) fun. TermLike term TyName Name uni fun => term ()
churchSucc :: forall term (uni :: Type -> Type) fun. TermLike term TyName Name uni fun => term ()

Documentation

churchNat :: forall (uni :: Type -> Type). Type TyName uni () Source #

Church-encoded Nat as a PLC type.

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

churchZero :: forall term (uni :: Type -> Type) fun. TermLike term TyName Name uni fun => term () Source #

Church-encoded '0' as a PLC term.

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

churchSucc :: forall term (uni :: Type -> Type) fun. 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)