		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

*_

Construct a repetition of zero or more instances of an element.

Signature
(*_ x) → repetition
Arguments: x — Guard (element/rulename-p x).
Returns: repetition — Type (repetitionp repetition).

If a rule name is supplied, it is promoted to an element.

The name of this function is inspired by the ABNF notation *.

Definitions and Theorems

Function: *_

(defun *_ (x)
  (declare (xargs :guard (element/rulename-p x)))
  (b* ((element (if (elementp x)
                    x
                  (element-rulename x)))
       (range (make-repeat-range :min 0
                                 :max (nati-infinity))))
    (make-repetition :range range
                     :element element)))

Theorem: repetitionp-of-*_

(defthm repetitionp-of-*_
  (b* ((repetition (*_ x)))
    (repetitionp repetition))
  :rule-classes :rewrite)