• 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
          • 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
            • Pseudo-event-formp
            • Pseudo-event-form-listp
            • Directed-untranslate
            • Irrelevant-formals-info
            • Numbered-names
            • Context-message-pair
            • Prove$
            • Minimize-ruler-extenders
            • Paired-names
              • Make-paired-name
              • Paired-name-separator
            • Orelse
            • Fresh-name-in-world-with-$s
            • Encapsulate-report-errors
            • On-failure
            • Chk-irrelevant-formals-ok
            • Named-formulas
            • Pseudo-event-landmarkp
            • All-program-fns
            • All-logic-fns
            • Trans-eval-error-triple
            • Trans-eval-state
            • Pseudo-tests-and-callsp
            • User-interface
            • Pseudo-command-landmarkp
            • Pseudo-tests-and-calls-listp
            • Pseudo-command-formp
            • Orelse*
            • Identity-macro
          • Integer-range-fix
          • Minimize-ruler-extenders
          • Add-const-to-untranslate-preprocess
          • Unsigned-byte-fix
          • Signed-byte-fix
          • Defthmr
          • Paired-names
            • Make-paired-name
            • Paired-name-separator
          • 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

Paired-names

Utilities for paired names.

A paired name is a symbol consisting of three parts, in this order:

  1. A non-empty sequence of characters that is the first name of the pair.
  2. A non-empty sequence of characters that separates the two names of the pair. This character sequence is global but customizable.
  3. A non-empty sequence of characters that is the second name of the pair.

Examples of paired names are:

  • F-~>-G, where F is the first name, -~> is the separator, and G is the second name.
  • LOGIC-SORT-IS-EXEC-SORT, where LOGIC-SORT is the first name, -IS- is the separator, and EXEC-SORT is the second name.

Note that if the separator occurs in the first or second name, the paired name cannot be uniquely decomposed into its three constituents. For instance, if the separator is <->, there are two different ways to decompose ABC<->DEF<->GHI.

Paired names are useful, for instance, to denote theorems that state certain kinds of relations between functions (denoted by the first and second names of the pairs), where the separator describes the relation, e.g. F-~>-G could denote a theorem stating that the function F is transformed into an equivalent function G.

Subtopics

Make-paired-name
Construct a paired name.
Paired-name-separator
Separator of the names in a paired name.