		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-to-value

Convert a c$::const to a c::value-option.

Signature
(const-to-value const) → value?
Arguments: const — Guard (constp const).
Returns: value? — Type (c::value-optionp value?).

Definitions and Theorems

Function: const-to-value

(defun const-to-value (const)
  (declare (xargs :guard (constp const)))
  (let ((__function__ 'const-to-value))
    (declare (ignorable __function__))
    (const-case const
                :int (iconst-to-value const.unwrap)
                :otherwise nil)))

Theorem: value-optionp-of-const-to-value

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