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 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
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)) (integerp x))

`THE`

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