		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Coerce-iconst-info

Coerce a valud to iconst-info.

Signature
(coerce-iconst-info x) → info
Returns: info — Type (iconst-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-iconst-info

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

Theorem: iconst-infop-of-coerce-iconst-info

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