		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Backref-extract-substr

Signature
(backref-extract-substr x str) → substr
Arguments: x — Guard (backref-p x).; str — Guard (stringp str).
Returns: substr — Type (stringp substr).

Definitions and Theorems

Function: backref-extract-substr

(defun backref-extract-substr (x str)
  (declare (xargs :guard (and (backref-p x) (stringp str))))
  (declare (xargs :guard (backref-in-bounds x str)))
  (let ((__function__ 'backref-extract-substr))
    (declare (ignorable __function__))
    (b* (((backref x)))
      (subseq (lstrfix str)
              x.loc (+ x.loc x.len)))))

Theorem: stringp-of-backref-extract-substr

(defthm stringp-of-backref-extract-substr
  (b* ((substr (backref-extract-substr x str)))
    (stringp substr))
  :rule-classes :type-prescription)

Theorem: backref-extract-substr-of-backref-fix-x

(defthm backref-extract-substr-of-backref-fix-x
  (equal (backref-extract-substr (backref-fix x)
                                 str)
         (backref-extract-substr x str)))

Theorem: backref-extract-substr-backref-equiv-congruence-on-x

(defthm backref-extract-substr-backref-equiv-congruence-on-x
  (implies (backref-equiv x x-equiv)
           (equal (backref-extract-substr x str)
                  (backref-extract-substr x-equiv str)))
  :rule-classes :congruence)

Theorem: backref-extract-substr-of-str-fix-str

(defthm backref-extract-substr-of-str-fix-str
  (equal (backref-extract-substr x (acl2::str-fix str))
         (backref-extract-substr x str)))

Theorem: backref-extract-substr-streqv-congruence-on-str

(defthm backref-extract-substr-streqv-congruence-on-str
  (implies (acl2::streqv str str-equiv)
           (equal (backref-extract-substr x str)
                  (backref-extract-substr x str-equiv)))
  :rule-classes :congruence)