The example
ACL2 !>(app 7 27)illustrates the fact that while ACL2 is an untyped language the ACL2 evaluator can be configured so as to check ``types'' at runtime. We should not say ``types'' here but ``guards.'' Click here for a discussion of guards.ACL2 Error in TOP-LEVEL: The guard for the function symbol ENDP, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 7).
The guard on endp
requires its argument to be a true
list. Since 7 is not a true list, and since ACL2 is checking guards
in this example, an error is signaled by ACL2. How do you know
ACL2 is checking guards? Because the prompt tells us
(click here) with its ``!''.