SET-BACKCHAIN-LIMIT

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 500