Ensure that a non-empty list of types is a singleton, and return its only element.
(atj-type-list-to-type types) → type
In some cases, a non-empty list of types is expected to be a singleton. For instance, the type list may be the output types of a function that is known to return a single result. This utility can be used in these cases, to check the expectation for robustness, and to retrieve the single type from the singleton list.
Function:
(defun atj-type-list-to-type (types) (declare (xargs :guard (atj-type-listp types))) (declare (xargs :guard (consp types))) (let ((__function__ 'atj-type-list-to-type)) (declare (ignorable __function__)) (if (= (len types) 1) (atj-type-fix (car types)) (prog2$ (raise "Internal error: ~x0 is not a singleton list of types." types) (atj-type-irrelevant)))))
Theorem:
(defthm atj-typep-of-atj-type-list-to-type (b* ((type (atj-type-list-to-type types))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-list-to-type-of-atj-type-list-fix-types (equal (atj-type-list-to-type (atj-type-list-fix types)) (atj-type-list-to-type types)))
Theorem:
(defthm atj-type-list-to-type-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-type-list-to-type types) (atj-type-list-to-type types-equiv))) :rule-classes :congruence)