		Search-engine friendly clone of the ACL2 documentation.

Svexlist

Svex-nth

nth for svexlists, with proper fty-discipline.

Signature
(svex-nth n x) → expr
Arguments: n — Guard (natp n).; x — Guard (svexlist-p x).
Returns: expr — Type (svex-p expr).

Definitions and Theorems

Function: svex-nth

(defun svex-nth (n x)
  (declare (xargs :guard (and (natp n) (svexlist-p x))))
  (let ((__function__ 'svex-nth))
    (declare (ignorable __function__))
    (mbe :logic (svex-fix (nth n x))
         :exec
         (if (< n (len x))
             (nth n x)
           (svex-quote (4vec-x))))))

Theorem: svex-p-of-svex-nth

(defthm svex-p-of-svex-nth
  (b* ((expr (svex-nth n x)))
    (svex-p expr))
  :rule-classes :rewrite)

Theorem: svex-nth-of-nfix-n

(defthm svex-nth-of-nfix-n
  (equal (svex-nth (nfix n) x)
         (svex-nth n x)))

Theorem: svex-nth-nat-equiv-congruence-on-n

(defthm svex-nth-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (svex-nth n x)
                  (svex-nth n-equiv x)))
  :rule-classes :congruence)

Theorem: svex-nth-of-svexlist-fix-x

(defthm svex-nth-of-svexlist-fix-x
  (equal (svex-nth n (svexlist-fix x))
         (svex-nth n x)))

Theorem: svex-nth-svexlist-equiv-congruence-on-x

(defthm svex-nth-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svex-nth n x)
                  (svex-nth n x-equiv)))
  :rule-classes :congruence)