Theory word12-def

theory file

name word12-def
version 1.98
requires
meta.description Definition of 12-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.Word12"
meta.show "Data.Word12.Bits"
meta.show "Number.Natural"
meta.show "Probability.Random"
name main
imports
  • def
  • word
subs
2 subs
name def
article word12-def.art
name word
imports
  • def
package word-1.121
interpretation
interpretation
  • type "Data.Word.word" as "Data.Word12.word12"
  • const "Data.Word.*" as "Data.Word12.*"
  • const "Data.Word.+" as "Data.Word12.+"
  • const "Data.Word.-" as "Data.Word12.-"
  • const "Data.Word.<" as "Data.Word12.<"
  • const "Data.Word.<=" as "Data.Word12.<="
  • const "Data.Word.^" as "Data.Word12.^"
  • const "Data.Word.~" as "Data.Word12.~"
  • const "Data.Word.and" as "Data.Word12.and"
  • const "Data.Word.bit" as "Data.Word12.bit"
  • const "Data.Word.fromNatural" as "Data.Word12.fromNatural"
  • const "Data.Word.modulus" as "Data.Word12.modulus"
  • const "Data.Word.not" as "Data.Word12.not"
  • const "Data.Word.or" as "Data.Word12.or"
  • const "Data.Word.random" as "Data.Word12.random"
  • const "Data.Word.shiftLeft" as "Data.Word12.shiftLeft"
  • const "Data.Word.shiftRight" as "Data.Word12.shiftRight"
  • const "Data.Word.toNatural" as "Data.Word12.toNatural"
  • const "Data.Word.width" as "Data.Word12.width"
  • const "Data.Word.Bits.compare" as "Data.Word12.Bits.compare"
  • const "Data.Word.Bits.fromWord" as "Data.Word12.Bits.fromWord"
  • const "Data.Word.Bits.normal" as "Data.Word12.Bits.normal"
  • const "Data.Word.Bits.toWord" as "Data.Word12.Bits.toWord"
[evaluating…]