		Search-engine friendly clone of the ACL2 documentation.

Sin$c

Sin$c-nth

Concrete implementation of strin-nth.

Signature
(sin$c-nth n sin$c) → *
Arguments: n — Guard (natp n).; sin$c — Guard (sin$c-okp sin$c).

Definitions and Theorems

Function: sin$c-nth$inline

(defun sin$c-nth$inline (n sin$c)
  (declare (xargs :stobjs (sin$c)))
  (declare (xargs :guard (and (natp n) (sin$c-okp sin$c))))
  (let ((__function__ 'sin$c-nth))
    (declare (ignorable __function__))
    (b* (((the string str) (sin$c-str sin$c))
         ((the (unsigned-byte 60) pos)
          (sin$c-pos sin$c))
         ((the (unsigned-byte 60) len)
          (length str))
         ((the (integer 0 *) idx) (+ pos n))
         ((when (>= idx len)) nil))
      (the character (char str idx)))))

Theorem: sin-nth{correspondence}

(defthm sin-nth{correspondence}
  (implies (and (sin$corr sin$c sin)
                (natp n)
                (strin-p sin))
           (equal (sin$c-nth$inline n sin$c)
                  (strin-nth n sin))))