1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
<html>
<head><title>SET-DEFAULT-HINTS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-DEFAULT-HINTS</h2>set the default hints
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre><p>
Examples:
(set-default-hints '((computed-hint-1 clause)
(computed-hint-2 clause
stable-under-simplificationp)))
(set-default-hints nil)
</pre>
<p>
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical <a href="WORLD.html">world</a> and is so
recorded. It is <code><a href="LOCAL.html">local</a></code> to the book or <code><a href="ENCAPSULATE.html">encapsulate</a></code> form in which it
occurs (see <a href="SET-DEFAULT-HINTS_bang_.html">set-default-hints!</a> for a corresponding non-<code><a href="LOCAL.html">local</a></code> event).
<p>
<pre>
General Form:
(set-default-hints lst)
</pre>
where <code>lst</code> is a list. Generally speaking, the elements of
<code>lst</code> should be suitable for use as <code><a href="COMPUTED-HINTS.html">computed-hints</a></code>.<p>
Whenever a <code><a href="DEFTHM.html">defthm</a></code> or <code><a href="THM.html">thm</a></code> command is executed, the default
hints are appended to the right of any explicitly provided
<code>:</code><code><a href="HINTS.html">hints</a></code> in the command. The same applies to <code><a href="DEFUN.html">defun</a></code>s as well
(<code>:hints</code>, <code>:guard-hints</code>, and (for ACL2(r)) <code>:std-hints</code>). The hints
are then translated and processed just as though they had been explicitly
included.
Technically, we do not put restrictions on <code>lst</code>, beyond that it
is a true list. It would be legal to execute
<pre>
(set-default-hints '(("Goal" :use lemma23)))
</pre>
with the effect that the given hint is added to subsequent hints supplied
explicitly. An explicit "Goal" hint would, however, take priority, as
suggested by the mention above of ``appended to the right.''<p>
Note that <code>set-default-hints</code> sets the default hints as specified.
To add to or remove from the current default, see <a href="ADD-DEFAULT-HINTS.html">add-default-hints</a> and
see <a href="REMOVE-DEFAULT-HINTS.html">remove-default-hints</a>.<p>
Finally, note that the effects of <code>set-default-hints</code>,
<code><a href="ADD-DEFAULT-HINTS.html">add-default-hints</a></code>, and <code><a href="REMOVE-DEFAULT-HINTS.html">remove-default-hints</a></code> are <code><a href="LOCAL.html">local</a></code> 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 <code><a href="SET-DEFAULT-HINTS_bang_.html">set-default-hints!</a></code>,
<code><a href="ADD-DEFAULT-HINTS_bang_.html">add-default-hints!</a></code>, or <code><a href="REMOVE-DEFAULT-HINTS_bang_.html">remove-default-hints!</a></code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
