| 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 Source | Bounded instance; from 0 to 255 |
| Enum Word4 Source | Enum instance, trivial definitions. |
| Eq Word4 Source | |
| Integral Word4 Source | 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 Source | |
| Num Word4 Source | Num instance, merely lifts underlying 8-bit operation and casts back |
| Ord Word4 Source | |
| Read Word4 Source | Read instance. We read as an 8-bit word, and coerce |
| Real Word4 Source | Real instance simply uses the Word8 instance |
| Show Word4 Source | Show instance |
| Bits Word4 Source | Bits instance |
| Random Word4 Source | Random instance, used in quick-check |
| SymWord Word4 Source | SymWord instance, allowing this type to be used in proofs/sat etc. |
| HasKind Word4 Source | HasKind instance; simply returning the underlying kind for the type |
| SatModel Word4 Source | SatModel instance, merely uses the generic parsing method. |
| SDivisible SWord4 Source | SDvisible instance, using default methods |
| SDivisible Word4 Source | SDvisible instance, using 0-extension |
| SIntegral Word4 Source | SIntegral instance, using default methods |
| FromBits SWord4 Source | Conversion from bits |
| Splittable Word8 Word4 Source | Joiningsplitting tofrom Word8 |