		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Coerce-var-info

Coerce a value to var-info.

Signature
(coerce-var-info x) → info
Returns: info — Type (var-infop info).

This must be used when the value is expected to have that type. We raise a hard error if that is not the case.

Definitions and Theorems

Function: coerce-var-info

(defun coerce-var-info (x)
 (declare (xargs :guard t))
 (let ((__function__ 'coerce-var-info))
  (declare (ignorable __function__))
  (if (var-infop x)
      x
    (prog2$ (raise "Internal error: ~x0 does not satisfy VAR-INFOP."
                   x)
            (irr-var-info)))))

Theorem: var-infop-of-coerce-var-info

(defthm var-infop-of-coerce-var-info
  (b* ((info (coerce-var-info x)))
    (var-infop info))
  :rule-classes :rewrite)