Add-default-hints
Add to the default hints
Examples:
(add-default-hints '((computed-hint-1 clause)
(computed-hint-2 clause
stable-under-simplificationp)))
(add-default-hints '((computed-hint-3 id clause world))
:at-end t)
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 add-default-hints! for a corresponding non-local
event).
General Forms:
(add-default-hints lst)
(add-default-hints lst :at-end flg)
where lst is a list. Generally speaking, the elements of lst
should be suitable for use as computed-hints.
This event is completely analogous to set-default-hints, the
difference being that add-default-hints appends the indicated hints to
the front of the list of default hints, so that they are tried first —
or, if flg is supplied and evaluates to other than nil, at the end
of the list, so that they are tried last — rather than replacing
the default hints with the indicated hints. Each new hint is thus considered
after each existing hint when both are applied to the same goal. Also See
set-default-hints, see remove-default-hints, and see 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!.
For a related feature, which however is only for advanced system builders,
see override-hints.
