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

Copyright(C) 2013-2016, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellTrustworthy
LanguageHaskell2010
Extensions
  • MonoLocalBinds
  • ScopedTypeVariables
  • GADTs
  • GADTSyntax
  • DataKinds
  • FlexibleContexts
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll

CLaSH.Promoted.Nat

Description

 

Synopsis

Documentation

data SNat n Source #

Singleton value for a type-level natural number n

Constructors

KnownNat n => SNat (Proxy n) 

Instances

Show (SNat n) Source # 

Methods

showsPrec :: Int -> SNat n -> ShowS #

show :: SNat n -> String #

showList :: [SNat n] -> ShowS #

snat :: KnownNat n => SNat n Source #

Create a singleton literal 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

snatToInteger :: SNat n -> Integer Source #

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

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

Add two singleton natural numbers

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

Subtract two singleton natural numbers

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

Multiply two singleton natural numbers

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

Power of two singleton natural numbers

data UNat :: Nat -> * where Source #

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 Source #

Convert a singleton natural number to its unary representation

NB: Not synthesisable

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

Add two unary singleton natural numbers

NB: Not synthesisable

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

Multiply two unary singleton natural numbers

NB: Not synthesisable

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

Power of two unary singleton natural numbers

NB: Not synthesisable