• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
              • Escape
              • Swcase-list->value-list
              • Hex-digit-list->chars
              • Fundef-list->name-list
              • Literal
              • Path
              • Plain-string
              • String-element
              • Identifier
              • Funcall-option
              • Expression-option
              • Statement-option
              • Literal-option
              • Identifier-option
              • Hex-string
              • Hex-quad
                • Hex-quad-fix
                • Hex-quad-equiv
                • Make-hex-quad
                • Change-hex-quad
                • Hex-quad->4th
                • Hex-quad->3rd
                • Hex-quad->2nd
                • Hex-quad->1st
                • Hex-quadp
              • Hex-digit
              • Data-value
              • Data-item
              • Hex-pair
              • Statements-to-fundefs
              • String-element-list-result
              • Identifier-identifier-map-result
              • Swcase-result
              • String-element-result
              • Statement-result
              • Literal-result
              • Identifier-set-result
              • Identifier-result
              • Identifier-list-result
              • Hex-pair-list-result
              • Fundef-result
              • Funcall-result
              • Expression-result
              • Escape-result
              • Path-result
              • Block-result
              • Objects
              • Statements/blocks/cases/fundefs
              • Identifier-list
              • Identifier-set
              • Identifier-identifier-map
              • Identifier-identifier-alist
              • String-element-list
              • Path-list
              • Hex-pair-list
              • Hex-digit-list
              • Literal-list
              • Fundef-list
              • Expressions/funcalls
              • Abstract-syntax-induction-schemas
            • Dynamic-semantics
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Number-theory
        • Cryptography
        • Lists-light
        • Builtins
        • Axe
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Abstract-syntax

Hex-quad

Fixtype of quadruples of hex digits.

This is a product type introduced by fty::defprod.

Fields
1st — hex-digit
2nd — hex-digit
3rd — hex-digit
4th — hex-digit

Subtopics

Hex-quad-fix
Fixing function for hex-quad structures.
Hex-quad-equiv
Basic equivalence relation for hex-quad structures.
Make-hex-quad
Basic constructor macro for hex-quad structures.
Change-hex-quad
Modifying constructor for hex-quad structures.
Hex-quad->4th
Get the 4th field from a hex-quad.
Hex-quad->3rd
Get the 3rd field from a hex-quad.
Hex-quad->2nd
Get the 2nd field from a hex-quad.
Hex-quad->1st
Get the 1st field from a hex-quad.
Hex-quadp
Recognizer for hex-quad structures.