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 uses the acl2-defaults-table, and hence its effect is
local to the book in which it occurs.
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 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 the :hints
argument of subsequent defthm events. But that would prevent
subsequent defthm events from having an explicitly provided
"Goal" hint 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;
it does not merely add to the current default. One might imagine a
set of convenient commands for manipulating the current setting but
in lieu of any experience with default hints we have implemented
only the most basic functionality.
