		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Strin-cdr

Advance the input stream by 1 character.

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

Definitions and Theorems

Function: strin-cdr

(defun strin-cdr (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-cdr))
    (declare (ignorable __function__))
    (b* (((strin x) x)
         (chars (strin-left x))
         ((when (atom chars))
          (change-strin x :chars nil))
         ((cons char1 rest) chars)
         ((when (eql char1 #\Newline))
          (change-strin x
                        :chars rest
                        :line (+ 1 x.line)
                        :col 0)))
      (change-strin x
                    :chars rest
                    :col (+ 1 x.col)))))

Theorem: strin-p-of-strin-cdr

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

Theorem: strin-left-of-strin-cdr

(defthm strin-left-of-strin-cdr
  (equal (strin-left (strin-cdr x))
         (cdr (strin-left x))))