		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-recognizer-all-conjuncts

Generate conjuncts for all members in the recognizer of the structures.

Signature
(defstruct-gen-recognizer-all-conjuncts memtypes) → terms
Arguments: memtypes — Guard (member-type-listp memtypes).
Returns: terms — A list of untranslated terms.
Type (true-listp terms).

This calls defstruct-gen-recognizer-conjuncts on all the members. See that function for details on the conjuncts.

Definitions and Theorems

Function: defstruct-gen-recognizer-all-conjuncts

(defun defstruct-gen-recognizer-all-conjuncts (memtypes)
 (declare (xargs :guard (member-type-listp memtypes)))
 (let ((__function__ 'defstruct-gen-recognizer-all-conjuncts))
  (declare (ignorable __function__))
  (cond
   ((endp memtypes) nil)
   (t
    (append
        (defstruct-gen-recognizer-conjuncts (car memtypes))
        (defstruct-gen-recognizer-all-conjuncts (cdr memtypes)))))))

Theorem: true-listp-of-defstruct-gen-recognizer-all-conjuncts

(defthm true-listp-of-defstruct-gen-recognizer-all-conjuncts
  (b* ((terms (defstruct-gen-recognizer-all-conjuncts memtypes)))
    (true-listp terms))
  :rule-classes :rewrite)

Theorem: defstruct-gen-recognizer-all-conjuncts-of-member-type-list-fix-memtypes

(defthm
 defstruct-gen-recognizer-all-conjuncts-of-member-type-list-fix-memtypes
 (equal (defstruct-gen-recognizer-all-conjuncts
             (member-type-list-fix memtypes))
        (defstruct-gen-recognizer-all-conjuncts memtypes)))

Theorem: defstruct-gen-recognizer-all-conjuncts-member-type-list-equiv-congruence-on-memtypes

(defthm
 defstruct-gen-recognizer-all-conjuncts-member-type-list-equiv-congruence-on-memtypes
 (implies
    (member-type-list-equiv memtypes memtypes-equiv)
    (equal (defstruct-gen-recognizer-all-conjuncts memtypes)
           (defstruct-gen-recognizer-all-conjuncts memtypes-equiv)))
 :rule-classes :congruence)