		Search-engine friendly clone of the ACL2 documentation.

Abnf-extensions

Make-repetition-0*-rule

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

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

Definitions and Theorems

Function: make-repetition-0*-rule

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

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

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