Theory word16-def

theory file

name word16-def
version 1.98
requires
meta.description Definition of 16-bit words
meta.author Joe Leslie-Hurd <joe@gilith.com>
meta.license MIT
meta.provenance HOL Light theory extracted on 2011-07-25
meta.show "Data.Bool"
meta.show "Data.List"
meta.show "Data.Word16"
meta.show "Data.Word16.Bits"
meta.show "Number.Natural"
meta.show "Probability.Random"
name main
imports
  • def
  • word
subs
2 subs
name def
article word16-def.art
name word
imports
  • def
package word-1.121
interpretation
interpretation
  • type "Data.Word.word" as "Data.Word16.word16"
  • const "Data.Word.*" as "Data.Word16.*"
  • const "Data.Word.+" as "Data.Word16.+"
  • const "Data.Word.-" as "Data.Word16.-"
  • const "Data.Word.<" as "Data.Word16.<"
  • const "Data.Word.<=" as "Data.Word16.<="
  • const "Data.Word.^" as "Data.Word16.^"
  • const "Data.Word.~" as "Data.Word16.~"
  • const "Data.Word.and" as "Data.Word16.and"
  • const "Data.Word.bit" as "Data.Word16.bit"
  • const "Data.Word.fromNatural" as "Data.Word16.fromNatural"
  • const "Data.Word.modulus" as "Data.Word16.modulus"
  • const "Data.Word.not" as "Data.Word16.not"
  • const "Data.Word.or" as "Data.Word16.or"
  • const "Data.Word.random" as "Data.Word16.random"
  • const "Data.Word.shiftLeft" as "Data.Word16.shiftLeft"
  • const "Data.Word.shiftRight" as "Data.Word16.shiftRight"
  • const "Data.Word.toNatural" as "Data.Word16.toNatural"
  • const "Data.Word.width" as "Data.Word16.width"
  • const "Data.Word.Bits.compare" as "Data.Word16.Bits.compare"
  • const "Data.Word.Bits.fromWord" as "Data.Word16.Bits.fromWord"
  • const "Data.Word.Bits.normal" as "Data.Word16.Bits.normal"
  • const "Data.Word.Bits.toWord" as "Data.Word16.Bits.toWord"
[evaluating…]