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
|
<html>
<head><title>MACRO-COMMAND.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>MACRO-COMMAND</h2>compound command for the proof-checker
<pre>Major Section: <a href="PROOF-CHECKER.html">PROOF-CHECKER</a>
</pre><p>
The proof-checker (see <a href="PROOF-CHECKER.html">proof-checker</a>) allows the user to supply
interactive commands. Compound commands, called macro commands, may
be defined; these expand into zero or more other commands. Some of
these are ``atomic'' macro commands; these are viewed as a single
command step when completed successfully.
<p>
More <a href="DOCUMENTATION.html">documentation</a> will be written on the <a href="PROOF-CHECKER.html">proof-checker</a>. For now,
we simply point out that there are lots of examples of the use of
<code>define-pc-macro</code> and <code>define-pc-atomic-macro</code> in the ACL2 source file
<code>"proof-checker-b.lisp"</code>. The former is used to create macro
commands, which can be submitted to the interactive loop
(see <a href="VERIFY.html">verify</a>) and will ``expand'' into zero or more commands.
The latter is similar, except that the undoing mechanism
(see <a href="ACL2-PC_colon__colon_UNDO.html">acl2-pc::undo</a>) understands atomic macro commands to
represent single interactive commands. Also see <a href="ACL2-PC_colon__colon_COMM.html">acl2-pc::comm</a>
and see <a href="ACL2-PC_colon__colon_COMMANDS.html">acl2-pc::commands</a> for a discussion of the display of
interactive commands.<p>
Also see <a href="TOGGLE-PC-MACRO.html">toggle-pc-macro</a> for how to change a macro command to
an atomic macro command, and vice versa.
<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>
|
