Return the list of the type names defined in a list of top-level constructs, in the same order.
(get-defined-type-names tops) → names
Function:
(defun get-defined-type-names (tops) (declare (xargs :guard (toplevel-listp tops))) (let ((__function__ 'get-defined-type-names)) (declare (ignorable __function__)) (b* (((when (endp tops)) nil) (top (car tops)) (names (toplevel-case top :type (list (type-definition->name top.get)) :types (get-defined-type-names-in-type-definitions (type-recursion->definitions top.get)) :function nil :functions nil :specification nil :theorem nil :transform nil)) (more-names (get-defined-type-names (cdr tops)))) (append names more-names))))
Theorem:
(defthm identifier-listp-of-get-defined-type-names (b* ((names (get-defined-type-names tops))) (identifier-listp names)) :rule-classes :rewrite)
Theorem:
(defthm defined-type-name-has-definition (implies (member-equal name (get-defined-type-names tops)) (type-definitionp (get-type-definition name tops))))
Theorem:
(defthm get-defined-type-names-of-toplevel-list-fix-tops (equal (get-defined-type-names (toplevel-list-fix tops)) (get-defined-type-names tops)))
Theorem:
(defthm get-defined-type-names-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (get-defined-type-names tops) (get-defined-type-names tops-equiv))) :rule-classes :congruence)