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

PlutusCore.StdLib.Data.Nat

Description

nat and related functions.

Synopsis

Documentation

natDataRecursiveType uni fun () Source #

Nat as a PLC type.

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

natTyType TyName uni () Source #

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

'0' as a PLC term.

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

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

succ as a PLC term.

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

foldrNatTermLike 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')

foldNatTermLike 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