• 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
            • 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
            • 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
          • 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
  • Kestrel-utilities
  • System-utilities-non-built-in

Numbered-names

Utilities for numbered names.

A numbered name is a symbol consisting of four parts, in this order:

  1. A non-empty base symbol.
  2. A non-empty sequence of non-numeric characters that marks the start of the numeric index, separating it from the base name. This character sequence is global but customizable.
  3. One of the following:
    • A non-empty sequence of numeric decimal digits not starting with 0, that forms the numeric index, which is a positive integer.
    • A non-empty sequence of non-numeric characters that forms a wildcard for the numeric index. This character sequence is global but customizable.
  4. A possibly empty sequence of non-numeric characters that marks the end of the numeric index and that, together with the character sequence in part 2 above, surrounds the numeric index or the wildcard. This character sequence is global but customizable.

Examples of numbered names are:

  • MUL2{14}, where MUL2 is the base name, { marks the start of the numeric index, 14 is the numeric index, and } marks the end of the numeric index.
  • SORT{*}, where SORT is the base name, { marks the start of the numeric index (wildcard), * is the wildcard, and } marks the end of the numeric index (wildcard).
  • FIND$3, where FIND is the base name, $ marks the start of the numeric index, 3 is the numeric index, and nothing marks the end of the numeric index.

Numbered names are useful, for instance, to denote subsequent versions of functions produced by sequences of transformations, e.g. foo{1}, foo{2}, ...

Subtopics

Check-numbered-name
Check if a symbol is a numbered name.
Next-numbered-name
Next numbered name with the same base.
Resolve-numbered-name-wildcard
Resolve the wildcard in a numbered name (if any) to the largest index in use for the name's base.
Set-numbered-name-index
Sets the index of a numbered name.
Next-fresh-numbered-names
Add to each of the given bases the lowest index, starting with the given index, such that the resulting names are not already in use.
Global-numbered-name-index
Global index for numbered names.
Make-numbered-name
Construct a numbered name from a base and an index (or wildcard).
Make-numbered-name-list
Lift make-numbered-name to lists.
Set-numbered-name-index-to-global
Sets the index of a numbered name to the global index for numbered names.
Numbered-names-in-use
Numbered names in use.
Next-fresh-numbered-name
Specialize next-fresh-numbered-names to a single name.
Numbered-name-index-wildcard
Wildcard for the numeric index of numbered names.
Numbered-name-index-start
Starting marker of the numeric index of numbered names.
Numbered-name-index-end
Ending marker of the numeric index of numbered names.