		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Value-result-to-option

Convert a c::value-result to a c::value-option.

Signature
(value-result-to-option result) → value?
Arguments: result — Guard (c::value-resultp result).
Returns: value? — Type (c::value-optionp value?).

Definitions and Theorems

Function: value-result-to-option

(defun value-result-to-option (result)
  (declare (xargs :guard (c::value-resultp result)))
  (let ((__function__ 'value-result-to-option))
    (declare (ignorable __function__))
    (if (c::errorp result)
        nil
      (c::value-fix result))))

Theorem: value-optionp-of-value-result-to-option

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