← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to doc/HTML/DECLARE.html

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HTML/DECLARE.html
1
1
<html>
2
 
<head><title>DECLARE.html  --  ACL2 Version 3.0.1</title></head>
 
2
<head><title>DECLARE.html  --  ACL2 Version 3.1</title></head>
3
3
<body text=#000000 bgcolor="#FFFFFF">
4
4
<h2>DECLARE</h2>declarations
5
5
<pre>Major Section:  <a href="PROGRAMMING.html">PROGRAMMING</a>
9
9
<pre>
10
10
Examples:
11
11
(declare (ignore x y z))
12
 
(declare (ignore x y z)
 
12
(declare (ignorable x y z)
13
13
         (type integer i j k)
14
14
         (type (satisfies integerp) m1 m2))
15
15
(declare (xargs :guard (and (integerp i)
22
22
where, in ACL2, each di is of one of the following forms:<p>
23
23
 
24
24
  (ignore v1 ... vn) -- where each vi is a variable introduced in
25
 
  the immediately superior lexical environment.<p>
26
 
 
27
 
  (type type-spec v1 ... vn) -- where each vi is a variable
28
 
  introduced in the immediately superior lexical environment and
29
 
  type-spec is a type specifier (as described in the documentation
30
 
  for <a href="TYPE-SPEC.html">type-spec</a>).<p>
31
 
 
32
 
  (xargs :key1 val1 ... :keyn valn) -- where the legal values of the
33
 
  keyi's and their respective vali's are described in the
34
 
  documentation for <a href="XARGS.html">xargs</a>.
 
25
  the immediately superior lexical environment.  These variables must not
 
26
  occur free in the scope of the declaration.<p>
 
27
 
 
28
  (ignorable v1 ... vn) -- where each vi is a variable introduced in
 
29
  the immediately superior lexical environment.  These variables need not
 
30
  occur free in the scope of the declaration.  This declaration can be useful
 
31
  for inhibiting compiler warnings.<p>
 
32
 
 
33
  (type type-spec v1 ... vn) -- where each vi is a variable introduced in the
 
34
  immediately superior lexical environment and type-spec is a type specifier
 
35
  (as described in the documentation for <a href="TYPE-SPEC.html">type-spec</a>).<p>
 
36
 
 
37
  (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's
 
38
  and their respective vali's are described in the documentation for
 
39
  <a href="XARGS.html">xargs</a>.
35
40
</pre>
36
41
 
37
42
Declarations in ACL2 may occur only where <code>dcl</code> occurs below:
43
48
  (MV-LET (v1 ...) term dcl ... dcl body)
44
49
</pre>
45
50
 
46
 
Of course, if a form macroexpands into one of these (as <code><a href="LET_star_.html">let*</a></code>
47
 
expands into nested <code><a href="LET.html">let</a></code>s and our <code>er-let*</code> expands into nested
48
 
<code><a href="MV-LET.html">mv-let</a></code>s) then declarations are permitted as handled by the macros
49
 
involved.<p>
 
51
Of course, if a form macroexpands into one of these (as <code><a href="LET_star_.html">let*</a></code> expands
 
52
into nested <code><a href="LET.html">let</a></code>s and our <code>er-let*</code> expands into nested <code><a href="MV-LET.html">mv-let</a></code>s)
 
53
then declarations are permitted as handled by the macros involved.<p>
50
54
 
51
 
<code>Declare</code> is defined in Common Lisp.  See any Common Lisp
52
 
documentation for more information.
 
55
<code>Declare</code> is defined in Common Lisp.  See any Common Lisp documentation for
 
56
more information.
53
57
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
54
58
</body>
55
59
</html>