Cardano.Plutus.DataSchema.Nat

data Z :: Natdata Z

Type level natural numbers. We need these for a variety of inductive "operations" (i.e. type classes w/ fundeps)

Instances

• KnownNat Z

data S :: Nat -> Natdata S t0

Instances

• (KnownNat n) => KnownNat (S n)

data Nat

The kind of type level natural number. This is not strictly needed, but improves the legibility of type errors and facilitates more comprehensible type signatures

class KnownNat :: Nat -> Constraintclass KnownNat n  where

PureScript version of the Haskell class defined in GHC.TypeLits. This is the Nat version of IsSymbol, more or less.

Members

• natVal :: Proxy n -> Int

Instances

• KnownNat Z
• (KnownNat n) => KnownNat (S n)