Find the definition of a type with a given name in a list of type definitions.
(get-type-definition-in-type-definitions name typedefs) → typedef?
This is used when looking up a type definition in a type recursion.
We return
We look up the definitions in order. In well-formed lists of type definitions, the type names are unique, so any order would yield the same result.
Function:
(defun get-type-definition-in-type-definitions (name typedefs) (declare (xargs :guard (and (identifierp name) (type-definition-listp typedefs)))) (let ((__function__ 'get-type-definition-in-type-definitions)) (declare (ignorable __function__)) (b* (((when (endp typedefs)) nil) ((when (identifier-equiv name (type-definition->name (car typedefs)))) (type-definition-fix (car typedefs)))) (get-type-definition-in-type-definitions name (cdr typedefs)))))
Theorem:
(defthm maybe-type-definitionp-of-get-type-definition-in-type-definitions (b* ((typedef? (get-type-definition-in-type-definitions name typedefs))) (maybe-type-definitionp typedef?)) :rule-classes :rewrite)
Theorem:
(defthm get-type-definition-in-type-definitions-of-identifier-fix-name (equal (get-type-definition-in-type-definitions (identifier-fix name) typedefs) (get-type-definition-in-type-definitions name typedefs)))
Theorem:
(defthm get-type-definition-in-type-definitions-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (get-type-definition-in-type-definitions name typedefs) (get-type-definition-in-type-definitions name-equiv typedefs))) :rule-classes :congruence)
Theorem:
(defthm get-type-definition-in-type-definitions-of-type-definition-list-fix-typedefs (equal (get-type-definition-in-type-definitions name (type-definition-list-fix typedefs)) (get-type-definition-in-type-definitions name typedefs)))
Theorem:
(defthm get-type-definition-in-type-definitions-type-definition-list-equiv-congruence-on-typedefs (implies (type-definition-list-equiv typedefs typedefs-equiv) (equal (get-type-definition-in-type-definitions name typedefs) (get-type-definition-in-type-definitions name typedefs-equiv))) :rule-classes :congruence)