|
|
|---|
|
|
|
|---|
Avoid removal of trivial equivalences during rewriting
This topic concerns an advanced control for the ACL2 prover.
This zero-ary attachable system function controls the
“remove-trivial-equivalences” heuristic, which uses an equality
hypothesis (and, when appropriate, an equivalence hypothesis) to
replace a variable by a term in the rest of the goal. (However, perhaps
similar heuristics will still be used, for example as part of the tau-system.) Attach the function