		Search-engine friendly clone of the ACL2 documentation.

Input-syntax-abstraction

Abs-*-input-section

Abstract a *input-item to a list of input items.

Signature
(abs-*-input-section trees) → initems
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: initems — Type (input-section-list-resultp initems).

Definitions and Theorems

Function: abs-*-input-section

(defun abs-*-input-section (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-input-section))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf insec)
          (abs-input-section (car trees)))
         ((okf insecs)
          (abs-*-input-section (cdr trees))))
      (if (null insec)
          insecs
        (cons insec insecs)))))

Theorem: input-section-list-resultp-of-abs-*-input-section

(defthm input-section-list-resultp-of-abs-*-input-section
  (b* ((initems (abs-*-input-section trees)))
    (input-section-list-resultp initems))
  :rule-classes :rewrite)

Theorem: abs-*-input-section-of-tree-list-fix-trees

(defthm abs-*-input-section-of-tree-list-fix-trees
  (equal (abs-*-input-section (abnf::tree-list-fix trees))
         (abs-*-input-section trees)))

Theorem: abs-*-input-section-tree-list-equiv-congruence-on-trees

(defthm abs-*-input-section-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (abs-*-input-section trees)
                  (abs-*-input-section trees-equiv)))
  :rule-classes :congruence)