Lift atj-type-to-keyword to lists.
(atj-type-list-to-keyword-list types) → kwds
Function:
(defun atj-type-list-to-keyword-list (types) (declare (xargs :guard (atj-type-listp types))) (let ((__function__ 'atj-type-list-to-keyword-list)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (cons (atj-type-to-keyword (car types)) (atj-type-list-to-keyword-list (cdr types)))))))
Theorem:
(defthm keyword-listp-of-atj-type-list-to-keyword-list (b* ((kwds (atj-type-list-to-keyword-list types))) (keyword-listp kwds)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-list-to-keyword-list-of-atj-type-list-fix-types (equal (atj-type-list-to-keyword-list (atj-type-list-fix types)) (atj-type-list-to-keyword-list types)))
Theorem:
(defthm atj-type-list-to-keyword-list-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-type-list-to-keyword-list types) (atj-type-list-to-keyword-list types-equiv))) :rule-classes :congruence)