• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
        • Linear
        • Definition
        • Clause-processor
          • Meta-extract
          • Set-skip-meta-termp-checks
          • Make-summary-data
          • Clause-processor-tools
            • Rp-rewriter
              • Rp-ruleset
              • Defthmrp
              • Rp-rewriter/meta-rules
              • Rp-utilities
                • Defthmrp
                • Show-rules
                • Def-rw-opener-error
                • Valid-sc
                • Set-rp-backchain-limit
                • Fetch-new-theory
                • Ex-from-rp
                • Rp-other-utilities
                • Rp-equal
                  • Rp-equal-cnt
                  • Rp-equal-cw
                    • Rp-equal-cw-subterms
                  • Rp-equal-subterms
                • Preserve-current-theory
                • Set-rw-step-limit
                • Rp-termp
                • Include-fnc
                • Set-rp-backchain-limit-throws-error
                • Defwarrant-rp
                • Create-case-match-macro
              • Rp-rewriter-demo
              • Rp-rewriter/debugging
              • Rp-rewriter/applications
          • Set-skip-meta-termp-checks!
        • Tau-system
        • Forward-chaining
        • Equivalence
        • Congruence
        • Free-variables
        • Executable-counterpart
        • Induction
        • Type-reasoning
        • Compound-recognizer
        • Rewrite-quoted-constant
        • Elim
        • Well-founded-relation-rule
        • Built-in-clause
        • Well-formedness-guarantee
        • Patterned-congruence
        • Rule-classes-introduction
        • Guard-holders
        • Refinement
        • Type-set-inverter
        • Generalize
        • Corollary
        • Induction-heuristics
        • Backchaining
        • Default-backchain-limit
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Rp-equal

Rp-equal-cw

Same as rp-equal but prints a mismatch.

Signature
(rp-equal-cw term1 term2) → *

Subtopics

Rp-equal-cw-subterms