Return the list of the type names defined in a list of definitions, in the same order.
(get-defined-type-names-in-type-definitions typedefs) → names
Function:
(defun get-defined-type-names-in-type-definitions (typedefs) (declare (xargs :guard (type-definition-listp typedefs))) (let ((__function__ 'get-defined-type-names-in-type-definitions)) (declare (ignorable __function__)) (cond ((endp typedefs) nil) (t (cons (type-definition->name (car typedefs)) (get-defined-type-names-in-type-definitions (cdr typedefs)))))))
Theorem:
(defthm identifier-listp-of-get-defined-type-names-in-type-definitions (b* ((names (get-defined-type-names-in-type-definitions typedefs))) (identifier-listp names)) :rule-classes :rewrite)
Theorem:
(defthm defined-type-name-in-type-definitions-has-definition (implies (member-equal name (get-defined-type-names-in-type-definitions typedefs)) (type-definitionp (get-type-definition-in-type-definitions name typedefs))))
Theorem:
(defthm get-defined-type-names-in-type-definitions-of-type-definition-list-fix-typedefs (equal (get-defined-type-names-in-type-definitions (type-definition-list-fix typedefs)) (get-defined-type-names-in-type-definitions typedefs)))
Theorem:
(defthm get-defined-type-names-in-type-definitions-type-definition-list-equiv-congruence-on-typedefs (implies (type-definition-list-equiv typedefs typedefs-equiv) (equal (get-defined-type-names-in-type-definitions typedefs) (get-defined-type-names-in-type-definitions typedefs-equiv))) :rule-classes :congruence)