THE

run-time type check 
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 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.