		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-elements

An elements parse tree is abstracted to its alternation.

Signature
(abstract-elements tree) → alternation
Arguments: tree — Guard (treep tree).
Returns: alternation — Type (alternationp alternation).

Definitions and Theorems

Function: abstract-elements

(defun abstract-elements (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (tree (car trees)))
    (abstract-alternation tree)))

Theorem: alternationp-of-abstract-elements

(defthm alternationp-of-abstract-elements
  (b* ((alternation (abstract-elements tree)))
    (alternationp alternation))
  :rule-classes :rewrite)