Locate the first occurrence of a substring.
(strpos x y) searches through the string
The function is "efficient" in the sense that it does not coerce its arguments into lists, but rather traverses both strings with char. On the other hand, it is a naive string search which operates by repeatedly calling strprefixp, rather than some better algorithm.
Corner case: we say that the empty string is a prefix of any other
string. That is,
(defun strpos$inline (x y) (declare (type string x y)) (mbe :logic (listpos (explode x) (explode y)) :exec (strpos-fast (the string x) (the string y) (the integer 0) (the integer (length (the string x))) (the integer (length (the string y))))))
(defthm streqv-implies-equal-strpos-1 (implies (streqv x x-equiv) (equal (strpos x y) (strpos x-equiv y))) :rule-classes (:congruence))
(defthm streqv-implies-equal-strpos-2 (implies (streqv y y-equiv) (equal (strpos x y) (strpos x y-equiv))) :rule-classes (:congruence))