Check if (the information for) a structure type has a flexible array member.
See tag-info for a description and a reference
to flexible array members.
If there are no members,
which cannot happen in well-formed structure types
(although we do not capture this invariant in tag-info),
we return
Function:
(defun tag-info-struct-flexiblep (info) (declare (xargs :guard (tag-infop info))) (declare (xargs :guard (tag-info-case info :struct))) (let ((__function__ 'tag-info-struct-flexiblep)) (declare (ignorable __function__)) (b* ((members (tag-info-struct->members info)) ((unless (consp members)) nil) (member (car (last members))) (type (member-type->type member))) (and (type-case type :array) (not (type-array->size type))))))
Theorem:
(defthm booleanp-of-tag-info-struct-flexiblep (b* ((yes/no (tag-info-struct-flexiblep info))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm tag-info-struct-flexiblep-of-tag-info-fix-info (equal (tag-info-struct-flexiblep (tag-info-fix info)) (tag-info-struct-flexiblep info)))
Theorem:
(defthm tag-info-struct-flexiblep-tag-info-equiv-congruence-on-info (implies (tag-info-equiv info info-equiv) (equal (tag-info-struct-flexiblep info) (tag-info-struct-flexiblep info-equiv))) :rule-classes :congruence)