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.
