		Search-engine friendly clone of the ACL2 documentation.

Constructor-utilities

Make-repetition-1*-rule

Makes ABNF AST for a repetition of one or more rulename.

Signature
(make-repetition-1*-rule rulename) → result
Arguments: rulename — Guard (common-lisp::stringp rulename).
Returns: result — Type (repetitionp result).

Definitions and Theorems

Function: make-repetition-1*-rule

(defun make-repetition-1*-rule (rulename)
  (declare (xargs :guard (common-lisp::stringp rulename)))
  (let ((__function__ 'make-repetition-1*-rule))
    (declare (ignorable __function__))
    (make-repetition :element (element-rulename (rulename rulename))
                     :range (make-repeat-range-1*))))

Theorem: repetitionp-of-make-repetition-1*-rule

(defthm repetitionp-of-make-repetition-1*-rule
  (b* ((result (make-repetition-1*-rule rulename)))
    (repetitionp result))
  :rule-classes :rewrite)