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

Information

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

Files

Defined Constants

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

Input Constants

Assumptions

T

() = λp. p = λx. T