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