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, and
otherwise, `val`

is the value of this expression. Here are some examples.

(the integer 3) ; returns 3 (the (integer 0 6) 3) ; returns 3 (the (integer 0 6) 7) ; causes an error (see below for exception)See type-spec for a discussion of the legal type specifications.

There is an exception to the rule that failure of the type-check causes an
error: there is no error when guard-checking has been turned off with
`:set-guard-checking :NONE`

or `(with-guard-checking :NONE ...)`

.
See set-guard-checking and see with-guard-checking.

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
expression, `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

`THE`

expression above is
as follows.
(implies (and (p1 x) (p2 x)) (let ((var x)) (integerp var)))

`THE`

is defined in Common Lisp. See any Common Lisp documentation
for more information.