Major Section: ACL2-BUILT-INS
(The typ val) checks that
val satisfies the type specification
typ (see type-spec). An error is caused if the check fails,
val is the value of this expression. Here are
(the integer 3) ; returns 3 (the (integer 0 6) 3) ; returns 3 (the (integer 0 6) 7) ; causes an errorSee type-spec for a discussion of the legal type specifications.
The following remark is for those who verify guards for their
functions (see guard and see verify-guards). We remark that a call of
(the TYPE EXPR) in the body of a function definition generates a guard
proof obligation that the type,
TYPE, holds for the value of the
EXPR. Consider the following example.
(defun f (x) (declare (xargs :guard (p1 x))) (if (p2 x) (the integer x) 17))The guard proof obligation generated for the
THEexpression above is as follows.
(implies (and (p1 x) (p2 x)) (integerp x))
THE is defined in Common Lisp. See any Common Lisp documentation
for more information.