(make-repeat-range-1*) → result
Function:
(defun make-repeat-range-1* nil (declare (xargs :guard t)) (let ((__function__ 'make-repeat-range-1*)) (declare (ignorable __function__)) (abnf::make-repeat-range :min 1 :max (acl2::nati-infinity))))
Theorem:
(defthm repeat-rangep-of-make-repeat-range-1* (b* ((result (make-repeat-range-1*))) (abnf::repeat-rangep result)) :rule-classes :rewrite)