substrp

(in-package "STR")

(include-book "strpos")

(local (include-book "arithmetic"))

(defsection substrp
  :parents (substrings)
  :short "Case-sensitive test for the existence of a substring."
  :long "<p>@(call substrp) determines if x ever occurs as a substring of y.
The test is case-sensitive.</p>

<p>See also @(see isubstrp) for a case-insensitive version, and @(see strpos)
or @(see strrpos) for alternatives that say where a match occurs.</p>"
  (definline substrp
    (x y)
    (declare (type string x y))
    (mbe :logic (sublistp (explode x) (explode y))
      :exec (if (strpos x y)
        t
        nil)))
  (defcong streqv
    equal
    (substrp x y)
    1)
  (defcong streqv
    equal
    (substrp x y)
    2))