Copyright | (c) Brian Huffman |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Demonstrates how new sizes of word/int types can be defined and used with SBV.
Documentation
Word4 as a newtype. Invariant: Word4 x
should satisfy x < 16
.
Bounded Word4 | Bounded instance; from 0 to 255 |
Enum Word4 | Enum instance, trivial definitions. |
Eq Word4 | |
Integral Word4 | Integral instance, again using Word8 instance and casting. NB. we do not need to use the smart constructor here as neither the quotient nor the remainder can overflow a Word4. |
Data Word4 | |
Num Word4 | Num instance, merely lifts underlying 8-bit operation and casts back |
Ord Word4 | |
Read Word4 | Read instance. We read as an 8-bit word, and coerce |
Real Word4 | Real instance simply uses the Word8 instance |
Show Word4 | Show instance |
Bits Word4 | Bits instance |
Random Word4 | Random instance, used in quick-check |
SymWord Word4 | SymWord instance, allowing this type to be used in proofs/sat etc. |
HasKind Word4 | HasKind instance; simply returning the underlying kind for the type |
SatModel Word4 | SatModel instance, merely uses the generic parsing method. |
SDivisible SWord4 | SDvisible instance, using default methods |
SDivisible Word4 | SDvisible instance, using 0-extension |
SIntegral Word4 | SIntegral instance, using default methods |
FromBits SWord4 | Conversion from bits |
Typeable * Word4 | |
Splittable Word8 Word4 | Joiningsplitting tofrom Word8 |