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