		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-alt-rest-comp

A (*c-wsp "/" *c-wsp concatenation) parse tree is abstracted to its concatenation.

Signature
(abstract-alt-rest-comp tree) → concatenation
Arguments: tree — Guard (treep tree).
Returns: concatenation — Type (concatenationp concatenation).

Function: abstract-alt-rest-comp

(defun abstract-alt-rest-comp (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))
                     (consp (cddr treess))
                     (consp (cdddr treess))))
        (fail))
       (trees (cadddr treess))
       ((unless (consp trees)) (fail))
       (tree (car trees)))
    (abstract-concatenation tree)))