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