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