clash-prelude-0.3: CAES Language for Synchronous Hardware - Prelude library

Safe HaskellNone
LanguageHaskell2010

CLaSH.Promoted.Nat

Synopsis

Documentation

data SNat n Source

Singleton value for a type-level natural number n

snat :: KnownNat n => SNat n Source

Singleton value for a type-level natural number

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

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

fromSNat :: SNat n -> Integer Source

Convert a singleton natural number to an integer

data UNat where Source

Unary representation of a type-level natural

Constructors

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

toUNat :: SNat n -> UNat n Source

Convert a singleton natural number to it's unary representation

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

Add two singleton natural numbers

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

Multiply two singleton natural numbers

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

Exponential of two singleton natural numbers