		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-alt-rest

A list of zero or more (*c-wsp "/" *c-wsp concatenation) parse trees is abstracted to the list of its concatenations (i.e. an alternation).

Signature
(abstract-alt-rest trees) → concatenations
Arguments: trees — Guard (tree-listp trees).
Returns: concatenations — Type (alternationp concatenations).

Function: abstract-alt-rest

(defun abstract-alt-rest (trees)
  (declare (xargs :guard (tree-listp trees)))
  (b* (((fun (fail)) (abstract-fail))
       ((when (endp trees)) nil)
       ((cons tree trees) trees)
       ((unless (tree-case tree :nonleaf))
        (fail))
       (concatenation (abstract-alt-rest-comp tree))
       (concatenations (abstract-alt-rest trees)))
    (cons concatenation concatenations)))