• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
        • Linear
        • Definition
        • Tau-system
        • Clause-processor
        • Forward-chaining
        • Equivalence
        • Free-variables
          • Add-match-free-override
          • Set-match-free-default
          • Free-variables-type-prescription
          • Set-match-free-error
          • Free-variables-examples
            • Free-variables-examples-rewrite
            • Free-variables-examples-forward-chaining
        • Congruence
        • Executable-counterpart
        • Induction
        • Compound-recognizer
        • Elim
        • Well-founded-relation-rule
        • Rewrite-quoted-constant
        • 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
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Real
      • ACL2-tutorial
      • Debugging
      • Miscellaneous
      • Output-controls
      • Built-in-theorems
      • Macros
      • Interfacing-tools
      • About-ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Free-variables

Free-variables-examples

Examples pertaining to free variables in rules

The examples in the two sub-topics of this topic illustrate the handling of free variables in rules of class :rewrite (see free-variables-examples-rewrite) and of class :forward-chaining (see free-variables-examples-forward-chaining), respectively. These implicitly illustrate free-variables handling in rules of class :linear as well. Also see free-variables and see rule-classes.

Subtopics

Free-variables-examples-rewrite
Examples pertaining to free variables in rewrite rules
Free-variables-examples-forward-chaining
Examples pertaining to free variables in forward-chaining rules