Names of the theorems asserting that flexible-array-member-p does not hold on a value of a given type.
(atc-type-to-notflexarrmem-thms type prec-tags) → notflexarrmem-thms
For an integer type, this is just one theorem related to that type's recognizer. For a pointer or an array, it is just one theorem for pointers. For a struct, it consists of the general theorem for structs, which has a hypothesis saying that the struct does not have a flexible array member, plus the theorem asserting that the struct in question does not have a flexible array member, needed to relieve the hypothesis; this is always used on structs without flexible array members.
Function:
(defun atc-type-to-notflexarrmem-thms (type prec-tags) (declare (xargs :guard (and (typep type) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-type-to-notflexarrmem-thms)) (declare (ignorable __function__)) (cond ((type-integerp type) (list (pack 'not-flexible-array-member-p-when- (atc-type-to-recognizer type prec-tags)))) ((or (type-case type :pointer) (type-case type :array)) (list 'not-flexible-array-member-p-when-value-pointer)) ((type-case type :struct) (list 'not-flexible-array-member-p-when-value-struct (defstruct-info->flexiblep-thm (atc-tag-info->defstruct (atc-get-tag-info (type-struct->tag type) prec-tags))))) (t (raise "Internal error: unexpected type ~x0." type)))))
Theorem:
(defthm symbol-listp-of-atc-type-to-notflexarrmem-thms (b* ((notflexarrmem-thms (atc-type-to-notflexarrmem-thms type prec-tags))) (symbol-listp notflexarrmem-thms)) :rule-classes :rewrite)