• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
        • Soft-future-work
        • Soft-macros
          • Defun-inst
          • Defequal
            • Defequal-implementation
              • Defequal-fn
              • Defequal-event-generation
              • Defequal-input-processing
              • Defequal-table
              • 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
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Defequal

Defequal-implementation

Implementation of defequal.

The implementation functions have arguments and results consistently named as follows (unless otherwise stated, explicitly or implicitly, in the functions):

  • name is the homonymous input to the event macro.
  • left is the homonymous input to the event macro.
  • right is the homonymous input to the event macro.
  • vars is the homonymous input to the event macro.
  • n is the arity of left and right, as described in the user documentation.
  • x1...xn is the list of variable symbols x1, ..., xn described in the user documentation.

Implementation functions' arguments and results that are not listed above are described in, or clear from, those functions' documentation.

Subtopics

Defequal-fn
Check redundancy, process the inputs, generated the events.
Defequal-event-generation
Event generation performed by defequal.
Defequal-input-processing
Input processing performed by defequal.
Defequal-table
Table that records successful defequal calls.
Defequal-macro-definition
Definition of the defequal macro.