Major Section: SWITCHES-PARAMETERS-AND-MODES
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, linear, meta, or type-prescription rule is
admitted. Its value may be a two-element list whose elements are each either
nil or a non-negative integer. Its value x may also be nil or a
non-negative integer, which is treated as the two element list (x x).
The first element of the list is used to limit backchaining for a rule of
class type-prescription while the second element is used to limit
backchaining for the other three classes of rules mentioned above.
See backchain-limit for details about how backchain-limits are used. The
examples below assume that a new rule doesn't itself specify a value for
:backchain-limit-lst.
:set-default-backchain-limit nil ; do not impose backchain limits for the
; rule
:set-default-backchain-limit 0 ; allow only type-set reasoning for
; relieving a new rule's hypotheses
:set-default-backchain-limit 500 ; allow backchaining through a new rewrite,
; linear, or meta rule's hypotheses to a
; depth of no more than 500
(set-default-backchain-limit 500) ; same as above
:set-default-backchain-limit (nil 500)
; same as above
(set-default-backchain-limit '(nil 500))
; same as above
(set-default-backchain-limit '(3 500))
; for a new :type-prescription rule, allow
; type-set backchaining to a depth
; of no more than 3; for a new
; rule of class :rewrite, :linear,
; or :meta, allow backchaining to
; a depth of no more than 50
(set-default-backchain-limit '(nil 500))
; do not limit backchaining for a
; new :type-prescription rule; for
; a new rule of class :rewrite,
; :linear, or :meta, allow
; backchaining to a depth of no
; more than 50
The initial default backchain-limit is nil.
