1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
<html>
<head><title>ILLEGAL.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ILLEGAL</h2>print an error message and stop execution
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>(Illegal ctx str alist)</code> causes evaluation to halt with a short
message using the ``context'' <code>ctx</code>. An error message is first printed
using the string <code>str</code> and alist <code>alist</code> that are of the same kind
as expected by <code><a href="FMT.html">fmt</a></code>. See <a href="FMT.html">fmt</a>, and see <a href="PROG2$.html">prog2$</a> for an
example of how to use a related function, <code><a href="HARD-ERROR.html">hard-error</a></code>
(see <a href="HARD-ERROR.html">hard-error</a>). Also see <a href="ER.html">er</a> for a macro that provides a unified
way of signaling errors.
<p>
The difference between <code>illegal</code> and <code><a href="HARD-ERROR.html">hard-error</a></code> is that the former
has a guard of <code>nil</code> while the latter has a <code><a href="GUARD.html">guard</a></code> of <code>t</code>. Thus,
you may want to use <code>illegal</code> rather than <code>hard-error</code> when you intend
to do <code><a href="GUARD.html">guard</a></code> verification at some point, and you expect the guard
to guarantee that the <code>illegal</code> call is never executed.
See <a href="PROG2$.html">prog2$</a> for an example.
<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>
|
