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
33
34
35
36
37
38
|
<html>
<head><title>ERROR1.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ERROR1</h2>print an error message and cause a ``soft error''
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>(Error1 ctx str alist)</code> returns <code>(mv t nil state)</code>. An error message is
first printed using the the ``context'' <code>ctx</code>, as well as 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>.<p>
<code>Error1</code> can be interpreted as causing an ``error'' when programming with
the ACL2 <code><a href="STATE.html">state</a></code>, something most ACL2 users will probably not want to do;
see <a href="LD-ERROR-TRIPLES.html">ld-error-triples</a> and see <a href="ER-PROGN.html">er-progn</a>. In order to cause errors with
<code>:</code><code><a href="LOGIC.html">logic</a></code> mode functions, see <a href="HARD-ERROR.html">hard-error</a> and see <a href="ILLEGAL.html">illegal</a>. Better
yet, see <a href="ER.html">er</a> for a macro that provides a unified way of signaling errors.
<p>
As mentioned above, <code>error1</code> always returns <code>(mv t nil state)</code>. But if a
call <code>(error1 ctx str alist)</code> is encountered during evaluation, then the
string <code>str</code> is first printed using the association list <code>alist</code> (as in
<code><a href="FMT.html">fmt</a></code>). Here is a trivial, contrived example.
<pre>
ACL2 !>(error1 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))
state)<p>
ACL2 Error in MY-CONTEXT: Printing 4: four<p>
ACL2 !>
</pre>
<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>
|
