		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-declaration

Abstract a *declaration to a list of top-level declarations.

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

Definitions and Theorems

Function: abs-*-declaration

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

Theorem: topdecl-list-resultp-of-abs-*-declaration

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

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

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

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

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