SET-DEFAULT-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. Moreover, its effect is to set the acl2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see acl2-defaults-table.

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
(set-default-backchain-limit 500) ; same as above

The initial default backchain-limit is nil.