plutus-core
Safe HaskellNone
LanguageHaskell2010

PlutusCore.StdLib.Data.Nat

Description

nat and related functions.

Synopsis

Documentation

natData :: forall (uni :: Type -> Type) fun. RecursiveType uni fun () Source #

Nat as a PLC type.

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

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

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

'0' as a PLC term.

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

succ :: forall term (uni :: Type -> Type) fun. 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 :: forall term (uni :: Type -> Type) fun. 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 :: forall term (uni :: Type -> Type) fun. 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 :: forall term (uni :: Type -> Type). (TermLike term TyName Name uni DefaultFun, HasTypeAndTermLevel uni Integer) => term () Source #

Convert a nat to an integer.

foldNat {integer} (addInteger 1) 1