Theory word-def

theory file

name word-def
version 1.81
requires
meta.description Definition of word operations
meta.author Joe Leslie-Hurd <joe@gilith.com>
meta.license MIT
meta.provenance HOL Light theory extracted on 2014-11-17
meta.show "Data.Bool"
meta.show "Data.Word"
meta.show "Number.Natural"
meta.show "Probability.Random"
name main
imports
  • def
  • modular
subs
2 subs
name def
article word-def.art
name modular
imports
  • def
package modular-1.92
interpretation
interpretation
  • type "Number.Modular.modular" as "Data.Word.word"
  • const "Number.Modular.*" as "Data.Word.*"
  • const "Number.Modular.+" as "Data.Word.+"
  • const "Number.Modular.-" as "Data.Word.-"
  • const "Number.Modular.<" as "Data.Word.<"
  • const "Number.Modular.<=" as "Data.Word.<="
  • const "Number.Modular.^" as "Data.Word.^"
  • const "Number.Modular.~" as "Data.Word.~"
  • const "Number.Modular.fromNatural" as "Data.Word.fromNatural"
  • const "Number.Modular.modulus" as "Data.Word.modulus"
  • const "Number.Modular.random" as "Data.Word.random"
  • const "Number.Modular.toNatural" as "Data.Word.toNatural"
[evaluating…]