(svdecomp-get-rewrite-limit state) → limit
Function:
(defun svdecomp-get-rewrite-limit (state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'svdecomp-get-rewrite-limit)) (declare (ignorable __function__)) (if (boundp-global 'svdecomp-rewrite-limit state) (nfix (f-get-global 'svdecomp-rewrite-limit state)) 5)))
Theorem:
(defthm natp-of-svdecomp-get-rewrite-limit (b* ((limit (svdecomp-get-rewrite-limit state))) (natp limit)) :rule-classes :type-prescription)