• 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-info
              • Make-defbyte-info
              • Change-defbyte-info
              • Make-honsed-defbyte-info
              • Honsed-defbyte-info
              • Defbyte-info->size
              • Defbyte-info->signed
            • Defbyte-check-size
            • Defbyte-fix-support-lemma
            • Defbyte-table
            • Defbyte-macro-definition
            • *defbyte-table-name*
        • Deffixequiv
        • Defresult
        • Deffixtype
        • Defoption
        • Fty-discipline
        • Fold
        • Fty-extensions
        • Defsubtype
        • Defset
        • Deftypes
        • Specific-types
        • Defflatsum
        • Deflist-of-len
        • Defbytelist
        • Fty::basetypes
        • Defomap
        • Defvisitors
        • Deffixtype-alias
        • Deffixequiv-sk
        • Defunit
        • Multicase
        • Deffixequiv-mutual
        • Fty::baselists
        • Def-enumcase
        • 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-implementation

Defbyte-infop

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

(defbyte-infop x) is a std::defaggregate of the following fields.

  • size — The size input.
        Invariant (or (posp size) (symbolp size) (and (acl2::tuplep 1 size) (symbolp (car size)))) .
  • signed — Whether the bytes are signed or not.
        Invariant (booleanp signed).

Source link: defbyte-infop

The name of the type is the key of the pair in the table.

Subtopics

Defbyte-info
Raw constructor for defbyte-infop structures.
Make-defbyte-info
Constructor macro for defbyte-infop structures.
Change-defbyte-info
A copying macro that lets you create new defbyte-infop structures, based on existing structures.
Make-honsed-defbyte-info
Constructor macro for honsed defbyte-infop structures.
Honsed-defbyte-info
Raw constructor for honsed defbyte-infop structures.
Defbyte-info->size
Access the size field of a defbyte-infop structure.
Defbyte-info->signed
Access the signed field of a defbyte-infop structure.