		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-import-declaration

Abstract a *declaration to a list of import declarations.

Signature
(abs-*-import-declaration trees) → defs
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: defs — Type (importdecl-list-resultp defs).

Definitions and Theorems

Function: abs-*-import-declaration

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

Theorem: importdecl-list-resultp-of-abs-*-import-declaration

(defthm importdecl-list-resultp-of-abs-*-import-declaration
  (b* ((defs (abs-*-import-declaration trees)))
    (importdecl-list-resultp defs))
  :rule-classes :rewrite)

Theorem: abs-*-import-declaration-of-tree-list-fix-trees

(defthm abs-*-import-declaration-of-tree-list-fix-trees
  (equal (abs-*-import-declaration (abnf::tree-list-fix trees))
         (abs-*-import-declaration trees)))

Theorem: abs-*-import-declaration-tree-list-equiv-congruence-on-trees

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