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 default backchain-limit used when a new
rewrite or linear rule is admitted. It must be nil or a
non-negative integer. (See backchain-limit for details.)
:set-default-backchain-limit nil ; do not impose additional limits
:set-default-backchain-limit 0 ; allow only type-reasoning for
; relieving hypotheses
:set-default-backchain-limit 500 ; allow backchaining to a depth of
; no more than 500