CLaSH.Promoted.Nat

Documentation

data SNat n

Singleton value for a type-level natural number n

• CLaSH.Promoted.Nat.Literals contains a list of predefined SNat literals
• CLaSH.Promoted.Nat.TH has functions to easily create large ranges of new SNat literals

Constructors

KnownNat n => SNat (Proxy n)

Instances

Show (SNat n)

snat :: KnownNat n => SNat n

Create a singleton literal for a type-level natural number

withSNat :: KnownNat n => (SNat n -> a) -> a

Supply a function with a singleton natural n according to the context

snatToInteger :: SNat n -> Integer

Reify the type-level Nat n to it's term-level Integer representation.

addSNat :: SNat a -> SNat b -> SNat (a + b)

Add two singleton natural numbers

subSNat :: SNat a -> SNat b -> SNat (a - b)

Subtract two singleton natural numbers

mulSNat :: SNat a -> SNat b -> SNat (a * b)

Multiply two singleton natural numbers

powSNat :: SNat a -> SNat b -> SNat (a ^ b)

Power of two singleton natural numbers

data UNat :: Nat -> * where

Unary representation of a type-level natural

NB: Not synthesisable

Constructors

UZero :: UNat 0

USucc :: UNat n -> UNat (n + 1)

toUNat :: SNat n -> UNat n

Convert a singleton natural number to its unary representation

NB: Not synthesisable

addUNat :: UNat n -> UNat m -> UNat (n + m)

Add two unary singleton natural numbers

NB: Not synthesisable

multUNat :: UNat n -> UNat m -> UNat (n * m)

Multiply two unary singleton natural numbers

NB: Not synthesisable

powUNat :: UNat n -> UNat m -> UNat (n ^ m)

Power of two unary singleton natural numbers

NB: Not synthesisable