		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-?repeat

A [repeat] parse tree is abstracted to its corresponding repetition range.

Signature
(abstract-?repeat tree) → range
Arguments: tree — Guard (treep tree).
Returns: range — Type (repeat-rangep range).

When the repeat subtree is absent, the tree is abstracted to the range from 1 to 1.

Definitions and Theorems

Function: abstract-?repeat

(defun abstract-?repeat (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (repeat-range 0 (nati-finite 0))))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((when (endp treess))
        (repeat-range 1 (nati-finite 1)))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees)))
    (abstract-repeat subtree)))

Theorem: repeat-rangep-of-abstract-?repeat

(defthm repeat-rangep-of-abstract-?repeat
  (b* ((range (abstract-?repeat tree)))
    (repeat-rangep range))
  :rule-classes :rewrite)