| Copyright | (c) Brian Huffman |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Examples.Misc.Word4
Description
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.
Instances
| 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 |