		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-program-item

Abstract a *program-item to a list of topdecl.

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

Definitions and Theorems

Function: abs-*-program-item

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

Theorem: topdecl-list-resultp-of-abs-*-program-item

(defthm topdecl-list-resultp-of-abs-*-program-item
  (b* ((defs (abs-*-program-item trees)))
    (topdecl-list-resultp defs))
  :rule-classes :rewrite)

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

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

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

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