Major Section: EVENTS
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
This event sets the global
backchain-limit used by the ACL2
rewriter. It must be
nil or a non-negative integer.
(See backchain-limit for details.)
:set-backchain-limit nil ; do not impose any additional limits :set-backchain-limit 0 ; allow only type reasoning for relieving ; hypotheses :set-backchain-limit 500 ; allow backchaining to a depth of no more ; than 500The default limit is