Package word16-def: word16-def

Information

name	word16-def
version	1.0
description	word16-def
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-02-19

Files

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

Defined Constant

Data
- Word16
  - Data.Word16.width

Theorem

⊦ Data.Word16.width =
  Number.Numeral.bit0
    (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