Assume-true-false-aggressive-p
Control rewriter's use of the type-alist with IF calls
This topic concerns an advanced control for the ACL2 prover.
This zero-ary attachable system function controls the rewriter's use of the
type-alist when diving into calls of IF. By default, when ACL2
rewrites what amounts to (if (or test1 test2) (if test1 _ x) _), the
type-alist will fail to note that test2 is true when rewriting x.
Attach the function constant-t-function-arity-0 to strengthen the use of
the type-alist so that test2 is instead noted as true in that case. Note
that this strengthening may slow down ACL2 considerably in some cases, and
should rarely if ever be necessary when calling the prover; but it can be
useful in applications that call the rewriter directly. Attach the function
constant-nil-function-arity-0 to restore the default behavior.
