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>
|