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
|
<html>
<head><title>DEFCONST.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFCONST</h2>define a constant
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Examples:
(defconst *digits* '(0 1 2 3 4 5 6 7 8 9))
(defconst *n-digits* (the unsigned-byte (length *digits*)))
<p>
General Form:
(defconst name term doc-string)
</pre>
where <code>name</code> is a symbol beginning and ending with the character <code>*</code>,
<code>term</code> is a variable-free term that is evaluated to determine the
value of the constant, and <code><a href="DOC-STRING.html">doc-string</a></code> is an optional <a href="DOCUMENTATION.html">documentation</a>
string (see <a href="DOC-STRING.html">doc-string</a>).<p>
When a constant symbol is used as a <a href="TERM.html">term</a>, ACL2 replaces it by
its value; see <a href="TERM.html">term</a>.<p>
It may be of interest to note that <code>defconst</code> is implemented at the
lisp level using <code>defparameter</code>, as opposed to <code>defconstant</code>.
(Implementation note: this is important for proper support of
undoing and redefinition.)
<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>
|
