Major Section: SWITCHES-PARAMETERS-AND-MODES
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded. Moreover, its effect is to set the
hence its effect is
local to the book or
containing it; see acl2-defaults-table.
This event sets the global
backchain-limit used by the ACL2 type-set
and rewriting mechanisms. Its value may be a cons whose car and cdr are each
nil or a non-negative integer. Its value
x may also be
nil or a non-negative integer, which is treated as a cons whose car and
cdr are both
The car is used to limit backchaining used by the ACL2 type-set mechanism, while the cdr is used to limit backchaining used by the rewriting mechanism. See backchain-limit for details about how backchain-limits are used.
:set-backchain-limit nil ; do not impose any additional limits :set-backchain-limit 0 ; allow only type-set reasoning for rewriting ; hypotheses :set-backchain-limit 500 ; allow backchaining to a depth of no more ; than 500 for rewriting hypotheses (set-backchain-limit 500) ; same as above :set-backchain-limit (500 500) ; same as above (set-backchain-limit '(500 500)) ; same as above (set-backchain-limit '(3 500)) ; allow type-set backchaining to a depth of no more ; than 3 and rewriter backchaining to a depth of no ; more than 500The default limit is