Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.StdLib.Data.Nat

Description

nat and related functions.

Synopsis

natData ∷ RecursiveType uni fun ()
natTy ∷ Type TyName uni ()
zero ∷ TermLike term TyName Name uni fun ⇒ term ()
succ ∷ TermLike term TyName Name uni fun ⇒ term ()
foldrNat ∷ TermLike term TyName Name uni fun ⇒ term ()
foldNat ∷ TermLike term TyName Name uni fun ⇒ term ()
natToInteger ∷ (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) ⇒ term ()

Documentation

natData ∷ RecursiveType uni fun () Source #

Nat as a PLC type.

fix \(nat :: *) -> all r. r -> (nat -> r) -> r

natTy ∷ Type TyName uni () Source #

zero ∷ TermLike term TyName Name uni fun ⇒ term () Source #

'0' as a PLC term.

wrapNat [] /\(r :: *) -> \(z : r) (f : nat -> r) -> z

succ ∷ TermLike term TyName Name uni fun ⇒ term () Source #

succ as a PLC term.

\(n : nat) -> wrapNat [] /\(r :: *) -> \(z : r) (f : nat -> r) -> f n

foldrNat ∷ TermLike term TyName Name uni fun ⇒ term () Source #

foldrNat as a PLC term.

/\(r :: *) -> \(f : r -> r) (z : r) ->
    fix {nat} {r} \(rec : nat -> r) (n : nat) ->
        unwrap n {r} z \(n' : nat) -> f (rec n')

foldNat ∷ TermLike term TyName Name uni fun ⇒ term () Source #

foldNat as a PLC term.

/\(r :: *) -> \(f : r -> r) ->
    fix {r} {nat -> r} \(rec : r -> nat -> r) (z : r) (n : nat) ->
        unwrap n {r} z (\(n' : nat) -> rec (f z) n')

natToInteger ∷ (TermLike term TyName Name uni DefaultFun, uni `HasTypeAndTermLevel` Integer) ⇒ term () Source #

Convert a nat to an integer.

foldNat {integer} (addInteger 1) 1