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
|
<html>
<head><title>ACL2-PC_colon__colon_USE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::USE</h3>(atomic macro)
<code> </code>use a lemma instance
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Example:
(USE true-listp-append
(:instance assoc-of-append (x a) (y b) (z c)))
-- Add two top-level hypotheses, one the lemma called
true-listp-append, and the other an instance of the lemma called
assoc-of-append by the substitution in which x is assigned a, y
is assigned b, and z is assigned c.
<p>
General Form:
(use &rest args)
</pre>
Add the given lemma instances to the list of top-level hypotheses.
See <a href="HINTS.html">hints</a> for the syntax of <code>:use</code> hints in <code>defthm</code>, which is
essentially the same as the syntax here (see the example above).<p>
This command calls the <code>prove</code> command, and hence should only be used
at the top of the conclusion.
<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>
|
