• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
          • Directed-untranslate
          • Include-book-paths
          • Ubi
          • Numbered-names
            • Check-numbered-name
            • Next-numbered-name
            • Resolve-numbered-name-wildcard
            • Set-numbered-name-index
            • Next-fresh-numbered-names
            • Global-numbered-name-index
            • Make-numbered-name
            • Make-numbered-name-list
            • Set-numbered-name-index-to-global
            • Numbered-names-in-use
              • Max-numbered-name-index-in-use
              • Add-numbered-name-in-use
            • Next-fresh-numbered-name
            • Numbered-name-index-wildcard
            • Numbered-name-index-start
            • Numbered-name-index-end
          • Digits-any-base
          • 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
          • Message-utilities
          • Book-runes-alist
          • User-interface
          • Bits/ubyte11s-digit-grouping
          • Bits/bytes-digit-grouping
          • Subsetp-eq-linear
          • Oset-utilities
          • Strict-merge-sort-<
          • Miscellaneous-enumerations
          • Maybe-unquote
          • Thm<w
          • Defthmd<w
          • Io-utilities
        • Set
        • C
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Numbered-names

Numbered-names-in-use

Numbered names in use.

A table keeps track of the numbered names “in use”. The table must be updated explicitly every time a new numbered name is used (e.g. introduced into the ACL2 world).

The table maps bases of numbered names to non-empty sets (encoded as lists) of positive integers. If base is mapped to (index1 ... indexN), it means that the numbered names with base base and indices index1, ..., indexN are in use.

Subtopics

Max-numbered-name-index-in-use
Largest index of numbered name in use with a given base.
Add-numbered-name-in-use
Record that a numbered name is in use.