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