File: Guessing_the_Type_of_a_Newly_Admitted_Function.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (26 lines) | stat: -rw-r--r-- 1,224 bytes parent folder | download
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
<html>
<head><title>Guessing_the_Type_of_a_Newly_Admitted_Function.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Guessing the Type of a Newly Admitted Function</h2>
<p>
When a function is admitted to the logic, ACL2 tries to ``guess''
what type of object it returns.  This guess is codified as a term
that expresses a property of the value of the function.  For <code>app</code>
the term is

<pre>
(OR (CONSP (APP X Y))
    (EQUAL (APP X Y) Y))
</pre>

which says that <code>app</code> returns either a cons or its second argument.
This formula is added to ACL2's rule base as a <code><a href="TYPE-PRESCRIPTION.html">type-prescription</a></code>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> rule.  Later we will discuss how rules are used by the ACL2
theorem prover.  The point here is just that when you add a definition,
the data base of rules is updated, not just by the addition of the
definitional axiom, but by several new rules.<p>

You should now return to <a href="Revisiting_the_Admission_of_App.html">the Walking Tour</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>