• 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
          • Soft-future-work
          • Soft-macros
            • Defun-inst
            • Defequal
              • Defequal-implementation
                • Defequal-fn
                • Defequal-event-generation
                • Defequal-input-processing
                • Defequal-table
                  • Defequal-trim-call
                  • Defequal-redundant?
                  • Defequal-record-call
                  • Defequal-trim-call-args
                • Defequal-macro-definition
            • Defsoft
            • Defthm-inst
            • Defun2
            • Defunvar
            • Defun-sk2
            • Defchoose2
            • Defthm-2nd-order
            • Define-sk2
            • Defund-sk2
            • Define2
            • Defund2
          • Updates-to-workshop-material
          • Soft-implementation
          • Soft-notions
        • 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
  • Defequal-implementation

Defequal-table

Table that records successful defequal calls.

This is used just to handle redundancy fow now.

The table uses defequal calls as keys, which it associates to their expansions (encapsulate) as values. The calls are stripped of the :print and :show-only options.

Subtopics

Defequal-trim-call
Trim a defequal call by removing the :print and :show-only inputs.
Defequal-redundant?
Check if a call of defequal is redundant, returning the associated expansion if it is.
Defequal-record-call
Table event to record a call of defequal.
Defequal-trim-call-args