		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-conc-rest

A list of zero or more (1*c-wsp repetition) parse trees is abstracted to the list of its repetitions (i.e. a concatenation).

Signature
(abstract-conc-rest trees) → repetitions
Arguments: trees — Guard (tree-listp trees).
Returns: repetitions — Type (concatenationp repetitions).

Function: abstract-conc-rest

(defun abstract-conc-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))
       (repetition (abstract-conc-rest-comp tree))
       (repetitions (abstract-conc-rest trees)))
    (cons repetition repetitions)))