Turn a single ATJ type into a singleton list of it.
(atj-type-to-type-list type) → types
This is just list, but we introduce an explicit function for greater clarity.
Function:
(defun atj-type-to-type-list (type) (declare (xargs :guard (atj-typep type))) (let ((__function__ 'atj-type-to-type-list)) (declare (ignorable __function__)) (list (atj-type-fix type))))
Theorem:
(defthm atj-type-listp-of-atj-type-to-type-list (b* ((types (atj-type-to-type-list type))) (atj-type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-type-to-type-list (b* ((types (atj-type-to-type-list type))) (consp types)) :rule-classes :type-prescription)
Theorem:
(defthm atj-type-to-type-list-of-atj-type-fix-type (equal (atj-type-to-type-list (atj-type-fix type)) (atj-type-to-type-list type)))
Theorem:
(defthm atj-type-to-type-list-atj-type-equiv-congruence-on-type (implies (atj-type-equiv type type-equiv) (equal (atj-type-to-type-list type) (atj-type-to-type-list type-equiv))) :rule-classes :congruence)