		Search-engine friendly clone of the ACL2 documentation.

Abnf-extensions

Make-repetition-unit-rule

Makes ABNF AST for a repetition of exactly one rulename.

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

Definitions and Theorems

Function: make-repetition-unit-rule

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

Theorem: repetitionp-of-make-repetition-unit-rule

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