Hey Wait! Is ACL2 Typed or Untyped?
ACL2 !>(app 7 27) 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).
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.'' See Guards in ACL2 for a discussion of guards.
The guard on endp