• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
          • Force
          • Hide
          • Syntaxp
          • 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
          • Bind-free
          • Loop-stopper
          • Backchain-limit
          • Double-rewrite
          • Rewrite-lambda-object
          • Rewriting-versus-cleaning-up-lambda-objects
          • Random-remarks-on-rewriting
          • Set-rw-cache-state
          • Case-split
          • Rewrite-lambda-object-actions
          • Syntactically-clean-lambda-objects-theory
          • Hands-off-lambda-objects-theory
          • Rewrite-lambda-objects-theory
          • Simple
          • Rewrite-stack-limit
          • Rewrite-equiv
          • Assume-true-false-aggressive-p
          • Remove-trivial-equivalences-enabled-p
          • Rewrite-lambda-modep
          • Rewrite-if-avoid-swap
          • Set-rw-cache-state!
          • Rw-cache-state
        • Meta
        • Linear
        • Definition
        • Clause-processor
        • Tau-system
        • Forward-chaining
        • Equivalence
        • Congruence
        • 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
        • 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
  • 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