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