Find the type of the field with a specified name.
(get-field-type name fields) → type?
We return the type of the first field found with the specified name. Well-formed lists of fields have unique names, so the first one found is also the only one (if present at all).
Function:
(defun get-field-type (name fields) (declare (xargs :guard (and (identifierp name) (field-listp fields)))) (let ((__function__ 'get-field-type)) (declare (ignorable __function__)) (b* (((when (endp fields)) nil) (field (car fields)) ((when (identifier-equiv name (field->name field))) (field->type field))) (get-field-type name (cdr fields)))))
Theorem:
(defthm maybe-typep-of-get-field-type (b* ((type? (get-field-type name fields))) (maybe-typep type?)) :rule-classes :rewrite)
Theorem:
(defthm get-field-type-of-identifier-fix-name (equal (get-field-type (identifier-fix name) fields) (get-field-type name fields)))
Theorem:
(defthm get-field-type-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (get-field-type name fields) (get-field-type name-equiv fields))) :rule-classes :congruence)
Theorem:
(defthm get-field-type-of-field-list-fix-fields (equal (get-field-type name (field-list-fix fields)) (get-field-type name fields)))
Theorem:
(defthm get-field-type-field-list-equiv-congruence-on-fields (implies (field-list-equiv fields fields-equiv) (equal (get-field-type name fields) (get-field-type name fields-equiv))) :rule-classes :congruence)