		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Strin-nthcdr

Advance the input stream by n characters.

Signature
(strin-nthcdr n x) → new-x
Arguments: n — Guard (natp n).; x — Guard (strin-p x).
Returns: new-x — Type (strin-p new-x), given the guard.

Definitions and Theorems

Function: strin-nthcdr

(defun strin-nthcdr (n x)
  (declare (xargs :guard (and (natp n) (strin-p x))))
  (let ((__function__ 'strin-nthcdr))
    (declare (ignorable __function__))
    (b* (((strin x) x)
         (chars (strin-left x))
         ((mv new-chars new-line new-col)
          (lc-nthcdr n chars x.line x.col)))
      (change-strin x
                    :chars new-chars
                    :line new-line
                    :col new-col))))

Theorem: strin-p-of-strin-nthcdr

(defthm strin-p-of-strin-nthcdr
  (implies (and (natp n) (strin-p x))
           (b* ((new-x (strin-nthcdr n x)))
             (strin-p new-x)))
  :rule-classes :rewrite)

Theorem: strin-left-of-strin-nthcdr

(defthm strin-left-of-strin-nthcdr
  (equal (strin-left (strin-nthcdr n x))
         (nthcdr n (strin-left x))))