File: USING-COMPUTED-HINTS.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (63 lines) | stat: -rw-r--r-- 1,887 bytes parent folder | download 
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>USING-COMPUTED-HINTS.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>USING-COMPUTED-HINTS</h2>how to use computed hints
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>

Computed hints are extraordinarily powerful.  We show a few examples
here to illustrate their use.  We recommend that these be read in
the following sequence:

<p>
<ul>
<li><h3><a href="ADD-DEFAULT-HINTS.html">ADD-DEFAULT-HINTS</a> -- add to the default hints
</h3>
</li>

<li><h3><a href="REMOVE-DEFAULT-HINTS.html">REMOVE-DEFAULT-HINTS</a> -- remove from the default hints
</h3>
</li>

<li><h3><a href="SET-DEFAULT-HINTS.html">SET-DEFAULT-HINTS</a> -- set the default hints
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-1.html">USING-COMPUTED-HINTS-1</a> -- Driving Home the Basics
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-2.html">USING-COMPUTED-HINTS-2</a> -- One Hint to Every Top-Level Goal in a Forcing Round
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-3.html">USING-COMPUTED-HINTS-3</a> -- Hints as a Function of the Goal (not its Name)
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-4.html">USING-COMPUTED-HINTS-4</a> -- Computing the Hints
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-5.html">USING-COMPUTED-HINTS-5</a> -- Debugging Computed Hints
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-6.html">USING-COMPUTED-HINTS-6</a> -- Using the computed-hint-replacement feature
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-7.html">USING-COMPUTED-HINTS-7</a> -- Using the <code>stable-under-simplificationp</code> flag
</h3>
</li>

<li><h3><a href="USING-COMPUTED-HINTS-8.html">USING-COMPUTED-HINTS-8</a> -- Some Final Comments
</h3>
</li>

</ul>


<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>