|
|
|---|
|
|
|
|---|
Extend the use of linear-arithmetic during rewriting
This topic concerns an advanced control for the ACL2 prover.
This zero-ary attachable system function supports extending the usual use
of linear-arithmetic during rewriting, specifically with the
test (first) argument of a call of