Package word16-bytes-def: Definition of 16-bit word to byte pair conversions
Information
| name | word16-bytes-def |
| version | 1.47 |
| description | Definition of 16-bit word to byte pair conversions |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-05-18 |
| requires | bool |
| show | Data.Bool Data.Byte Data.Pair Data.Word16 Number.Natural |
Files
- Package tarball word16-bytes-def-1.47.tgz
- Theory file word16-bytes-def.thy (included in the package tarball)
Defined Constants
- Data
- Word16
- fromBytes
- toBytes
- Word16
Theorems
⊦ ∀b1 b2.
fromBytes b1 b2 =
or (shiftLeft (fromNatural (toNatural b1)) 8)
(fromNatural (toNatural b2))
⊦ ∀w.
toBytes w =
(fromNatural (toNatural (shiftRight w 8)),
fromNatural (toNatural (and w 255)))
Input Type Operators
- →
- bool
- Data
- Byte
- byte
- Pair
- ×
- Word16
- word16
- Byte
- Number
- Natural
- natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ⊤
- Byte
- fromNatural
- toNatural
- Pair
- ,
- Word16
- and
- fromNatural
- or
- shiftLeft
- shiftRight
- toNatural
- Bool
- Number
- Natural
- bit0
- bit1
- zero
- Natural
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤