		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-sparseint-val

Signature
(s4vec-sparseint-val x &key (__function__ '__function__)) → val
Arguments: x — Guard (sparseint-p x).
Returns: val — Type (equal val (sparseint-val x)).

Definitions and Theorems

Function: s4vec-sparseint-val$inline

(defun s4vec-sparseint-val$inline (x __function__)
  (declare (xargs :guard (sparseint-p x)))
  (b* ((xlen (sparseint-length x))
       (- (and (<= (s4vec-bit-limit) xlen)
               (s4vec-very-large-integer-warning xlen))))
    (sparseint-val x)))

Theorem: return-type-of-s4vec-sparseint-val

(defthm return-type-of-s4vec-sparseint-val
  (b* ((val (s4vec-sparseint-val$inline x __function__)))
    (equal val (sparseint-val x)))
  :rule-classes :rewrite)

Theorem: s4vec-sparseint-val$inline-of-sparseint-fix-x

(defthm s4vec-sparseint-val$inline-of-sparseint-fix-x
  (equal (s4vec-sparseint-val$inline (sparseint-fix x)
                                     __function__)
         (s4vec-sparseint-val$inline x __function__)))

Theorem: s4vec-sparseint-val$inline-sparseint-equiv-congruence-on-x

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