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.
General Form: (set-default-hints lst)where
lstis a list. Generally speaking, the element of
lstshould be suitable for use as
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
hintsargument of subsequent
defthmevents. But that would prevent subsequent
defthmevents 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
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.