		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-conc-rest-comp

A (1*c-wsp repetition) parse tree is abstracted to its repetition.

Signature
(abstract-conc-rest-comp tree) → repetition
Arguments: tree — Guard (treep tree).
Returns: repetition — Type (repetitionp repetition).

Function: abstract-conc-rest-comp

(defun abstract-conc-rest-comp (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (repetition (repeat-range 0 (nati-finite 0))
                            (element-group nil))))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))))
        (fail))
       (trees (cadr treess))
       ((unless (consp trees)) (fail))
       (tree (car trees)))
    (abstract-repetition tree)))