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>COMMAND.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>COMMAND</h2>forms you type at the top-level, but...
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
...the word ``command'' usually refers to a top-level form whose
evaluation produces a new logical <a href="WORLD.html">world</a>.
<pre>
Typical commands are:
(defun foo (x) (cons x x))
(defthm consp-foo (consp (foo x)))
(defrec pair (hd . tl) nil)
</pre>
The first two forms are examples of commands that are in fact
primitive <a href="EVENTS.html">events</a>. See <a href="EVENTS.html">events</a>. <code>Defrec</code>, on the other hand, is a
macro that expands into a <code><a href="PROGN.html">progn</a></code> of several primitive <a href="EVENTS.html">events</a>. In
general, a <a href="WORLD.html">world</a> extending command generates one or more <a href="EVENTS.html">events</a>.
<p>
Both <a href="EVENTS.html">events</a> and commands leave landmarks on the <a href="WORLD.html">world</a> that enable us
to determine how the given <a href="WORLD.html">world</a> was created from the previous one.
Most of your interactions will occur at the command level, i.e., you
type commands, you print previous commands, and you undo back
through commands. Commands are denoted by command descriptors.
See <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a>.
<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>
|
