SET-DEFAULT-BACKCHAIN-LIMIT

sets the default backchain-limit used when admitting a rule
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

The initial default backchain-limit is nil.