Guessing the Type of a Newly Admitted Function
Guessing the Type of a Newly Admitted Function
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 app the term
is
(OR (CONSP (APP X Y))
(EQUAL (APP X Y) Y))
which says that app returns either a cons or its second argument.
This formula is added to ACL2's rule base as a type-prescription
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 database of rules
is updated, not just by the addition of the definitional axiom, but by several
new rules.
You should now return to the Walking Tour.
