		Search-engine friendly clone of the ACL2 documentation.

Substrings

Substrp

Case-sensitive test for the existence of a substring.

(substrp x y) determines if x ever occurs as a substring of y. The test is case-sensitive.

See also isubstrp for a case-insensitive version, and strpos or strrpos for alternatives that say where a match occurs.

Definitions and Theorems

Function: substrp$inline

(defun substrp$inline (x y)
  (declare (type string x y))
  (mbe :logic (sublistp (explode x) (explode y))
       :exec (if (strpos x y) t nil)))

Theorem: streqv-implies-equal-substrp-1

(defthm streqv-implies-equal-substrp-1
  (implies (streqv x x-equiv)
           (equal (substrp x y)
                  (substrp x-equiv y)))
  :rule-classes (:congruence))

Theorem: streqv-implies-equal-substrp-2

(defthm streqv-implies-equal-substrp-2
  (implies (streqv y y-equiv)
           (equal (substrp x y)
                  (substrp x y-equiv)))
  :rule-classes (:congruence))