Package byte-def: byte-def

Information

Files

• Package tarball byte-def-1.0.tgz
• Theory file byte-def.thy (included in the package tarball)

Defined Constant

• Data
  • Byte
    • Data.Byte.width

Theorem

⊦ Data.Byte.width =
  Number.Numeral.bit0
    (Number.Numeral.bit0
       (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))

Input Type Operators

• →
• bool
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Number
  • Numeral
    • Number.Numeral.bit0
    • Number.Numeral.bit1
    • Number.Numeral.zero