		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Iconst-to-value

Signature
(iconst-to-value iconst) → value?
Arguments: iconst — Guard (c$::iconstp iconst).
Returns: value? — Type (c::value-optionp value?).

Definitions and Theorems

Function: iconst-to-value

(defun iconst-to-value (iconst)
  (declare (xargs :guard (c$::iconstp iconst)))
  (let ((__function__ 'iconst-to-value))
    (declare (ignorable __function__))
    (value-result-to-option
         (c::eval-iconst (c$::ldm-iconst iconst)))))

Theorem: value-optionp-of-iconst-to-value

(defthm value-optionp-of-iconst-to-value
  (b* ((value? (iconst-to-value iconst)))
    (c::value-optionp value?))
  :rule-classes :rewrite)