		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Strin-left

Remaining characters in a strin-p.

Signature
(strin-left x) → chars
Arguments: x — Guard (strin-p x).
Returns: chars — Type (character-listp chars).

This is an alternative to strin->chars that charlist-fixes the characters. This is generally preferable to using strin->chars directly, and allows us to avoid strin-p hyps in many theorems.

Definitions and Theorems

Function: strin-left

(defun strin-left (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-left))
    (declare (ignorable __function__))
    (mbe :logic (charlist-fix (strin->chars x))
         :exec (strin->chars x))))

Theorem: character-listp-of-strin-left

(defthm character-listp-of-strin-left
  (b* ((chars (strin-left x)))
    (character-listp chars))
  :rule-classes :rewrite)

Theorem: true-listp-of-strin-left

(defthm true-listp-of-strin-left
  (true-listp (strin-left x))
  :rule-classes :type-prescription)

Theorem: strin-left-of-make-strin

(defthm strin-left-of-make-strin
  (equal (strin-left (make-strin :chars chars
                                 :line line
                                 :col col
                                 :file file))
         (charlist-fix chars)))