String.isInfixOf

Stream: Is there code for X?

[Joachim Breitner]

Is there a function String → String → bool that tells me whether s1 is a substring of s2?

[Adam Topaz]

see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/String.2EcontainsSubstring/near/371008174

[Adam Topaz]

the shortest implementation seems to be s1.toList <:+: s2.toList

[Adam Topaz]

(that's a prop though)

[Joachim Breitner]

Thanks. I just wrote

def String.isInfixOf (needle : String) (hey : String) := Id.run do
  let mut i := hey.mkIterator
  while not i.atEnd do
    if needle.isPrefixOf i.remainingToString
    then return true
    else i := i.next
  return false

to be unblocked for now, and will maybe use https://github.com/leanprover/std4/pull/178 when it lands.

[Joachim Breitner]

(This thread is resolved for me…)