		Search-engine friendly clone of the ACL2 documentation.

Values

Type-of-value-option

Type of an optional value.

Signature
(type-of-value-option val?) → type
Arguments: val? — Guard (value-optionp val?).
Returns: type — Type (typep type).

This is the type of the value if the value is present, while it is void if the value is absent. This is a handy extension of type-of-value, given that, in the dynamic semantics, we model computations that may return void (e.g. function calls) as returning optional values, with nil for no value.

Definitions and Theorems

Function: type-of-value-option

(defun type-of-value-option (val?)
  (declare (xargs :guard (value-optionp val?)))
  (let ((__function__ 'type-of-value-option))
    (declare (ignorable __function__))
    (value-option-case val?
                       :some (type-of-value val?.val)
                       :none (type-void))))

Theorem: typep-of-type-of-value-option

(defthm typep-of-type-of-value-option
  (b* ((type (type-of-value-option val?)))
    (typep type))
  :rule-classes :rewrite)

Theorem: type-of-value-option-of-value-option-fix-val?

(defthm type-of-value-option-of-value-option-fix-val?
  (equal (type-of-value-option (value-option-fix val?))
         (type-of-value-option val?)))

Theorem: type-of-value-option-value-option-equiv-congruence-on-val?

(defthm type-of-value-option-value-option-equiv-congruence-on-val?
  (implies (value-option-equiv val? val?-equiv)
           (equal (type-of-value-option val?)
                  (type-of-value-option val?-equiv)))
  :rule-classes :congruence)