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