• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
        • Force
        • Hide
        • Syntaxp
        • Free-variables
        • 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
      • 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

• Rewrite

Rewrite-lambda-modep

switch controlling rewriting of lambda objects

Rewrite-lambda-modep is an identity function with no purpose other than to serve as a switch controlling whether and how the ACL2 prover rewrites quoted lambda objects in argument positions of ilk :FN. Behavior is determined by the enabled status of two runes associated with rewrite-lambda-modep, the executable-counterpart rune and the definition rune. See rewrite-lambda-object.