		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

1*_

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

Signature
(1*_ 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 1*.

Definitions and Theorems

Function: 1*_

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

Theorem: repetitionp-of-1*_

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