Copyright | (C) 2013-2016 University of Twente 2016-2019 Myrtle Software Ltd |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
Safe Haskell | Unsafe |
Language | Haskell2010 |
Extensions |
|
Synopsis
- newtype Index (n :: Nat) = I {}
- fromSNat :: (KnownNat m, n <= (m + 1)) => SNat n -> Index m
- size# :: (KnownNat n, 1 <= n) => Index n -> Int
- pack# :: Index n -> BitVector (CLog 2 n)
- unpack# :: (KnownNat n, 1 <= n) => BitVector (CLog 2 n) -> Index n
- eq# :: Index n -> Index n -> Bool
- neq# :: Index n -> Index n -> Bool
- lt# :: Index n -> Index n -> Bool
- ge# :: Index n -> Index n -> Bool
- gt# :: Index n -> Index n -> Bool
- le# :: Index n -> Index n -> Bool
- enumFrom# :: forall n. KnownNat n => Index n -> [Index n]
- enumFromThen# :: forall n. KnownNat n => Index n -> Index n -> [Index n]
- enumFromTo# :: Index n -> Index n -> [Index n]
- enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
- maxBound# :: forall n. KnownNat n => Index n
- (+#) :: KnownNat n => Index n -> Index n -> Index n
- (-#) :: KnownNat n => Index n -> Index n -> Index n
- (*#) :: KnownNat n => Index n -> Index n -> Index n
- fromInteger# :: KnownNat n => Integer -> Index n
- plus# :: Index m -> Index n -> Index ((m + n) - 1)
- minus# :: Index m -> Index n -> Index ((m + n) - 1)
- times# :: Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
- quot# :: Index n -> Index n -> Index n
- rem# :: Index n -> Index n -> Index n
- toInteger# :: Index n -> Integer
- resize# :: KnownNat m => Index n -> Index m
Datatypes
newtype Index (n :: Nat) Source #
Arbitrary-bounded unsigned integer represented by ceil(log_2(n))
bits.
Given an upper bound n
, an Index
n
number has a range of: [0 .. n
-1]
>>>
maxBound :: Index 8
7>>>
minBound :: Index 8
0>>>
read (show (maxBound :: Index 8)) :: Index 8
7>>>
1 + 2 :: Index 8
3>>>
2 + 6 :: Index 8
*** Exception: X: Clash.Sized.Index: result 8 is out of bounds: [0..7] ...>>>
1 - 3 :: Index 8
*** Exception: X: Clash.Sized.Index: result -2 is out of bounds: [0..7] ...>>>
2 * 3 :: Index 8
6>>>
2 * 4 :: Index 8
*** Exception: X: Clash.Sized.Index: result 8 is out of bounds: [0..7] ...
I | The constructor, |
Instances
Construction
Accessors
Length information
Type classes
BitPack
Eq
Ord
Enum (not synthesizable)
Bounded
Num
ExtendingNum
Integral
toInteger# :: Index n -> Integer Source #