• 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
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
            • Renaming-variables
            • Dead-code-eliminator
            • Renamings
              • Renaming
                • Renamingp
                • Renaming-fix
                • Renaming-equiv
                • Make-renaming
                • Renaming->list
                • Change-renaming
              • Renaming-result
              • Renaming-old
              • Renaming-new
              • Renaming-pair-equality
            • Disambiguator
            • Unique-variables
            • Dead-code-eliminator-static-safety
            • No-function-definitions
            • Unique-functions
            • Renaming-functions
            • Dead-code-eliminator-no-loop-initializers
            • Dead-code-eliminator-no-function-definitions
            • No-loop-initializers
            • For-loop-init-rewriter
          • Language
          • Yul-json
        • 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
  • Renamings

Renaming

Fixtype of renamings.

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

Fields
list — identifier-identifier-alist
Additional Requirements

The following invariant is enforced on the fields:

(and (no-duplicatesp-equal (strip-cars list)) 
     (no-duplicatesp-equal (strip-cdrs list))) 

These are alists from identifiers to identifiers that have unique keys and unique values, which we treat as lists of pairs rather than as alists as such (see discussion in renamings). We wrap the alist into a one-component product type and we add constraints for key and value uniqueness.

Subtopics

Renamingp
Recognizer for renaming structures.
Renaming-fix
Fixing function for renaming structures.
Renaming-equiv
Basic equivalence relation for renaming structures.
Make-renaming
Basic constructor macro for renaming structures.
Renaming->list
Get the list field from a renaming.
Change-renaming
Modifying constructor for renaming structures.