• 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
          • Omaps
          • Directed-untranslate
          • Include-book-paths
          • Ubi
          • Numbered-names
          • Digits-any-base
            • Defdigits
              • Defdigits-implementation
                • Defdigits-fn
                • Defdigits-infop
                  • Defdigits-info
                  • Make-defdigits-info
                  • Honsed-defdigits-info
                  • Change-defdigits-info
                  • Make-honsed-defdigits-info
                  • Defdigits-info->digits-pred-correct
                  • Defdigits-info->digits-fix-correct
                  • Defdigits-info->digits-description
                  • Defdigits-info->digit-pred-correct
                  • Defdigits-info->nat-to-lendian
                  • Defdigits-info->nat-to-bendian
                  • Defdigits-info->lendian-to-nat
                  • Defdigits-info->digits-pred
                  • Defdigits-info->digits-fix
                  • Defdigits-info->digit-pred
                  • Defdigits-info->digit-fix-correct
                  • Defdigits-info->digit-fix
                  • Defdigits-info->bendian-to-nat
                  • Defdigits-info->base
                • Defdigits-macro-definition
                • Defdigits-table
                • *defdigits-table-name*
            • Nat=>lendian*
            • Group-lendian
            • Defdigit-grouping
            • Ungroup-lendian
            • Lendian=>nat
            • Defthm-dab-return-types
            • Bendian=>nat
            • Nat=>bendian*
            • Trim-bendian*
            • Trim-lendian*
            • Nat=>lendian
            • Dab-digit-list-fix
            • Nat=>bendian
            • Ungroup-bendian
            • Group-bendian
            • Digits=>nat-injectivity-theorems
            • Dab-digit-listp
            • Nat=>lendian+
            • Dab-basep
            • Nat=>bendian+
            • Digits=>nat=>digits-inverses-theorems
            • Trim-lendian+
            • Trim-bendian+
            • Nat=>digits=>nat-inverses-theorems
            • Dab-digitp
            • Group/ungroup-inverses-theorems
            • Dab-digit-fix
            • Nat=>digits-injectivity-theorems
            • Dab-base
            • Digits-any-base-pow2
            • Dab-base-fix
          • Context-message-pair
          • With-auto-termination
          • Make-termination-theorem
          • Theorems-about-true-list-lists
          • Checkpoint-list
          • Sublis-expr+
          • Integers-from-to
          • Prove$
          • Defthm<w
          • System-utilities-non-built-in
          • Integer-range-fix
          • Minimize-ruler-extenders
          • Add-const-to-untranslate-preprocess
          • Unsigned-byte-fix
          • Signed-byte-fix
          • Defthmr
          • Paired-names
          • Unsigned-byte-list-fix
          • Signed-byte-list-fix
          • Show-books
          • Skip-in-book
          • Typed-tuplep
          • List-utilities
          • Checkpoint-list-pretty
          • Defunt
          • Keyword-value-list-to-alist
          • Magic-macroexpand
          • Top-command-number-fn
          • Bits-as-digits-in-base-2
          • Show-checkpoint-list
          • Ubyte11s-as-digits-in-base-2048
          • Named-formulas
          • Bytes-as-digits-in-base-256
          • String-utilities
          • Make-keyword-value-list-from-keys-and-value
          • Defmacroq
          • Integer-range-listp
          • Apply-fn-if-known
          • Trans-eval-error-triple
          • Checkpoint-info-list
          • Previous-subsumer-hints
          • Fms!-lst
          • Zp-listp
          • Trans-eval-state
          • Injections
          • Doublets-to-alist
          • Theorems-about-osets
          • Typed-list-utilities
          • Book-runes-alist
          • User-interface
          • Bits/ubyte11s-digit-grouping
          • Bits/bytes-digit-grouping
          • Message-utilities
          • Subsetp-eq-linear
          • Oset-utilities
          • Strict-merge-sort-<
          • Miscellaneous-enumerations
          • Maybe-unquote
          • Thm<w
          • Defthmd<w
          • Io-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Defdigits-implementation

Defdigits-infop

Information about a successful defdigits call, recorded as a pair's value in the defdigits table.

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

  • base — Invariant (dab-basep base).
  • digit-pred — Invariant (symbolp digit-pred).
  • digit-fix — Invariant (symbolp digit-fix).
  • digits-pred — Invariant (symbolp digits-pred).
  • digits-fix — Invariant (symbolp digits-fix).
  • bendian-to-nat — Invariant (symbolp bendian-to-nat).
  • lendian-to-nat — Invariant (symbolp lendian-to-nat).
  • nat-to-bendian — Invariant (symbolp nat-to-bendian).
  • nat-to-lendian — Invariant (symbolp nat-to-lendian).
  • digits-description — Invariant (stringp digits-description).
  • digit-pred-correct — Invariant (symbolp digit-pred-correct).
  • digit-fix-correct — Invariant (symbolp digit-fix-correct).
  • digits-pred-correct — Invariant (symbolp digits-pred-correct).
  • digits-fix-correct — Invariant (symbolp digits-fix-correct).

Source link: defdigits-infop

The name input of the defdigits call is the key of the pair in the table. Each field of this aggregate except the last two corresponds to the input of defdigits with the same name. The last two fields are the names of two theorems generated by defdigits.

Subtopics

Defdigits-info
Raw constructor for defdigits-infop structures.
Make-defdigits-info
Constructor macro for defdigits-infop structures.
Honsed-defdigits-info
Raw constructor for honsed defdigits-infop structures.
Change-defdigits-info
A copying macro that lets you create new defdigits-infop structures, based on existing structures.
Make-honsed-defdigits-info
Constructor macro for honsed defdigits-infop structures.
Defdigits-info->digits-pred-correct
Access the digits-pred-correct field of a defdigits-infop structure.
Defdigits-info->digits-fix-correct
Access the digits-fix-correct field of a defdigits-infop structure.
Defdigits-info->digits-description
Access the digits-description field of a defdigits-infop structure.
Defdigits-info->digit-pred-correct
Access the digit-pred-correct field of a defdigits-infop structure.
Defdigits-info->nat-to-lendian
Access the nat-to-lendian field of a defdigits-infop structure.
Defdigits-info->nat-to-bendian
Access the nat-to-bendian field of a defdigits-infop structure.
Defdigits-info->lendian-to-nat
Access the lendian-to-nat field of a defdigits-infop structure.
Defdigits-info->digits-pred
Access the digits-pred field of a defdigits-infop structure.
Defdigits-info->digits-fix
Access the digits-fix field of a defdigits-infop structure.
Defdigits-info->digit-pred
Access the digit-pred field of a defdigits-infop structure.
Defdigits-info->digit-fix-correct
Access the digit-fix-correct field of a defdigits-infop structure.
Defdigits-info->digit-fix
Access the digit-fix field of a defdigits-infop structure.
Defdigits-info->bendian-to-nat
Access the bendian-to-nat field of a defdigits-infop structure.
Defdigits-info->base
Access the base field of a defdigits-infop structure.