		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-get-rewrite-limit

Signature
(svdecomp-get-rewrite-limit state) → limit
Returns: limit — Type (natp limit).

Definitions and Theorems

Function: svdecomp-get-rewrite-limit

(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: natp-of-svdecomp-get-rewrite-limit

(defthm natp-of-svdecomp-get-rewrite-limit
  (b* ((limit (svdecomp-get-rewrite-limit state)))
    (natp limit))
  :rule-classes :type-prescription)