		Search-engine friendly clone of the ACL2 documentation.

Abnf-extensions

Make-repetition-unit-case-sensitive-string

Makes ABNF AST for a repetition of exactly one instance of the given case-sensitive string terminal.).

Signature
(make-repetition-unit-case-sensitive-string string) → result
Arguments: string — Guard (stringp string).
Returns: result — Type (abnf::repetitionp result).

Definitions and Theorems

Function: make-repetition-unit-case-sensitive-string

(defun make-repetition-unit-case-sensitive-string (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'make-repetition-unit-case-sensitive-string))
    (declare (ignorable __function__))
    (abnf::make-repetition
         :element
         (abnf::element-char-val (abnf::char-val-sensitive string))
         :range (make-repeat-range-1*1))))

Theorem: repetitionp-of-make-repetition-unit-case-sensitive-string

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