Ensure that a list of types is a singleton.
(ensure-single-type types) → type?
If the check is successful, return the type.
Otherwise, we return
This is used to ensure that an expression is single-valued. We call this function on the type list in the type-result resulting from checking the static well-formedness of the expression.
Function:
(defun ensure-single-type (types) (declare (xargs :guard (type-listp types))) (let ((__function__ 'ensure-single-type)) (declare (ignorable __function__)) (and (consp types) (not (consp (cdr types))) (type-fix (car types)))))
Theorem:
(defthm maybe-typep-of-ensure-single-type (b* ((type? (ensure-single-type types))) (maybe-typep type?)) :rule-classes :rewrite)
Theorem:
(defthm ensure-single-type-of-type-list-fix-types (equal (ensure-single-type (type-list-fix types)) (ensure-single-type types)))
Theorem:
(defthm ensure-single-type-type-list-equiv-congruence-on-types (implies (type-list-equiv types types-equiv) (equal (ensure-single-type types) (ensure-single-type types-equiv))) :rule-classes :congruence)