Major Section: EVENTS
Examples: (set-default-hints '((computed-hint-1 clause) (computed-hint-2 clause stable-under-simplificationp))) (set-default-hints nil)
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so
recorded. It is local to the book or encapsulate form in which it
occurs (see set-default-hints! for a corresponding non-local event).
General Form: (set-default-hints lst)where
lst is a list. Generally speaking, the element of
lst should be suitable for use as computed-hints.
Whenever a defthm or thm command is executed, the default
hints are appended to the right of any explicitly provided
:hints in the command. The same applies to defuns as well
(:hints, :guard-hints, and (for ACL2(r)) :std-hints). The hints
are then translated and processed just as though they had been explicitly
included.
Technically, we do not put restrictions on lst, beyond that it
is a true list. It would be legal to execute
(set-default-hints '(("Goal" :use lemma23)))
with the effect that the given hint is added to subsequent hints supplied
explicitly. But that would prevent subsequent events from having an
explicitly provided "Goal" hints since it is illegal to provide two
hints on the same goal-spec. We strongly recommend that you keep the
default hints set to a list of computed-hints.
Note that set-default-hints sets the default hints as specified.
To add to or remove from the current default, see add-default-hints and
see remove-default-hints.
Finally, note that the effects of set-default-hints,
add-default-hints, and remove-default-hints are local to the
book in which they appear. Thus, users who include a book with such forms
will not have their default hints affected by such forms. In order to export
the effect of setting the default hints, use set-default-hints!,
add-default-hints!, or remove-default-hints!.
