(vl-make-package-with-parse-error name minloc maxloc err tokens) → package
Function:
(defun vl-make-package-with-parse-error (name minloc maxloc err tokens) (declare (xargs :guard (and (stringp name) (vl-location-p minloc) (vl-location-p maxloc) (vl-warning-p err) (vl-tokenlist-p tokens)))) (let ((__function__ 'vl-make-package-with-parse-error)) (declare (ignorable __function__)) (b* ((warn2 (make-vl-warning :type :vl-parse-error :msg "[[ Remaining ]]: ~s0 ~s1.~%" :args (list (vl-tokenlist->string-with-spaces (take (min 4 (len tokens)) (list-fix tokens))) (if (> (len tokens) 4) "..." "")) :fatalp t :fn __function__))) (make-vl-package :name name :minloc minloc :maxloc maxloc :warnings (list err warn2)))))
Theorem:
(defthm vl-package-p-of-vl-make-package-with-parse-error (b* ((package (vl-make-package-with-parse-error name minloc maxloc err tokens))) (vl-package-p package)) :rule-classes :rewrite)