		Search-engine friendly clone of the ACL2 documentation.

Input-syntax-abstraction

Abs-*-input-item

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

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

Definitions and Theorems

Function: abs-*-input-item

(defun abs-*-input-item (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-input-item))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf initem)
          (abs-input-item (car trees)))
         ((okf initems)
          (abs-*-input-item (cdr trees))))
      (cons initem initems))))

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

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

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

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

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

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