Like nth but, with proper fty-discipline for 4veclists. ``Safely'' causes a run-time error if
(4veclist-nth-safe n x) → elt
Function:
(defun 4veclist-nth-safe (n x) (declare (xargs :guard (and (natp n) (4veclist-p x)))) (let ((__function__ '4veclist-nth-safe)) (declare (ignorable __function__)) (mbe :logic (4vec-fix (nth n x)) :exec (or (nth n x) (raise "Index ~x0 too large for 4veclist of length ~x1." n (len x)) (4vec-x)))))
Theorem:
(defthm 4vec-p-of-4veclist-nth-safe (b* ((elt (4veclist-nth-safe n x))) (4vec-p elt)) :rule-classes :rewrite)
Theorem:
(defthm 4veclist-nth-safe-of-nfix-n (equal (4veclist-nth-safe (nfix n) x) (4veclist-nth-safe n x)))
Theorem:
(defthm 4veclist-nth-safe-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (4veclist-nth-safe n x) (4veclist-nth-safe n-equiv x))) :rule-classes :congruence)
Theorem:
(defthm 4veclist-nth-safe-of-4veclist-fix-x (equal (4veclist-nth-safe n (4veclist-fix x)) (4veclist-nth-safe n x)))
Theorem:
(defthm 4veclist-nth-safe-4veclist-equiv-congruence-on-x (implies (4veclist-equiv x x-equiv) (equal (4veclist-nth-safe n x) (4veclist-nth-safe n x-equiv))) :rule-classes :congruence)
Theorem:
(defthm 4veclist-nth-safe-of-nil (equal (4veclist-nth-safe n nil) (4vec-x)))
Theorem:
(defthm 4veclist-nth-safe-of-cons (implies (syntaxp (quotep n)) (equal (4veclist-nth-safe n (cons a b)) (if (zp n) (4vec-fix a) (4veclist-nth-safe (1- n) b)))))
Theorem:
(defthm 4veclist-nth-safe-out-of-bounds (implies (<= (len x) (nfix n)) (equal (4veclist-nth-safe n x) (4vec-x))))