• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
        • Defbytelist
        • Defbyte-standard-instances
        • Defbyte-ihs-theorems
        • Defbyte-implementation
          • Defbyte-fn
          • Defbyte-infop
          • Defbyte-check-size
          • Defbyte-fix-support-lemma
          • Defbyte-table
          • Defbyte-macro-definition
          • *defbyte-table-name*
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Defomap
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defbyte

Defbyte-implementation

Implementation of defbyte.

Subtopics

Defbyte-fn

Events generated by defbyte.

Defbyte-infop

Information about a defbyte type, recorded as a pair's value in the defbyte table.

Defbyte-check-size

Check if the size input is valid.

Defbyte-fix-support-lemma

Support lemma for generated fixing theorem.

Defbyte-table

Table of defbyte types.

Defbyte-macro-definition

Definition of the defbyte macro.

*defbyte-table-name*

Name of the defbyte table.