		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-length

Signature
(sparseint$-length x) → length
Arguments: x — Guard (sparseint$-p x).

Definitions and Theorems

Function: sparseint$-length$inline

(defun sparseint$-length$inline (x)
  (declare (xargs :guard (sparseint$-p x)))
  (let ((__function__ 'sparseint$-length))
    (declare (ignorable __function__))
    (b* ((tail/len (sparseint$-length-rec x)))
      (max tail/len 0))))

Theorem: sparseint$-length-correct

(defthm sparseint$-length-correct
  (b* ((common-lisp::?length (sparseint$-length$inline x)))
    (equal length
           (integer-length (sparseint$-val x)))))

Theorem: sparseint$-length$inline-of-sparseint$-fix-x

(defthm sparseint$-length$inline-of-sparseint$-fix-x
  (equal (sparseint$-length$inline (sparseint$-fix x))
         (sparseint$-length$inline x)))

Theorem: sparseint$-length$inline-sparseint$-equiv-congruence-on-x

(defthm sparseint$-length$inline-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-length$inline x)
                  (sparseint$-length$inline x-equiv)))
  :rule-classes :congruence)