Package word16-bytes-def: Definition of 16-bit word to byte pair conversions

Information

nameword16-bytes-def
version1.70
descriptionDefinition of 16-bit word to byte pair conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-11-10
requiresbool
byte
natural
pair
word16-def
showData.Bool
Data.Byte
Data.Pair
Data.Word16
Number.Natural

Files

Defined Constants

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)

Input Type Operators

Input Constants

Assumptions

() = λp. p = λx.