		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-comma-struct-component-declaration

Abstract a *( "," struct-component-declaration ) to a list of compdecl.

Signature
(abs-*-comma-struct-component-declaration trees) → ret-comps
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: ret-comps — Type (compdecl-list-resultp ret-comps).

Definitions and Theorems

Function: abs-*-comma-struct-component-declaration

(defun abs-*-comma-struct-component-declaration (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-comma-struct-component-declaration))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf comp)
          (abs-comma-struct-component-declaration (car trees)))
         ((okf comps)
          (abs-*-comma-struct-component-declaration (cdr trees))))
      (cons comp comps))))

Theorem: compdecl-list-resultp-of-abs-*-comma-struct-component-declaration

(defthm
  compdecl-list-resultp-of-abs-*-comma-struct-component-declaration
  (b* ((ret-comps (abs-*-comma-struct-component-declaration trees)))
    (compdecl-list-resultp ret-comps))
  :rule-classes :rewrite)

Theorem: compdecl-listp-of-abs-*-comma-struct-component-declaration

(defthm compdecl-listp-of-abs-*-comma-struct-component-declaration
 (b* ((?ret-comps (abs-*-comma-struct-component-declaration trees)))
   (implies (not (reserrp ret-comps))
            (compdecl-listp ret-comps))))

Theorem: abs-*-comma-struct-component-declaration-of-tree-list-fix-trees

(defthm
    abs-*-comma-struct-component-declaration-of-tree-list-fix-trees
  (equal (abs-*-comma-struct-component-declaration
              (abnf::tree-list-fix trees))
         (abs-*-comma-struct-component-declaration trees)))

Theorem: abs-*-comma-struct-component-declaration-tree-list-equiv-congruence-on-trees

(defthm
 abs-*-comma-struct-component-declaration-tree-list-equiv-congruence-on-trees
 (implies
     (abnf::tree-list-equiv trees trees-equiv)
     (equal (abs-*-comma-struct-component-declaration trees)
            (abs-*-comma-struct-component-declaration trees-equiv)))
 :rule-classes :congruence)