feat(library/init/data/string): add String.isPrefixOf

library/init/data/string/basic.lean

@@ -312,6 +312,18 @@ s.foldl (λ n c, n*10 + (c.toNat - '0'.toNat)) 0
 def isNat (s : String) : Bool :=
 s.all $ λ c, c.isDigit
 
+partial def isPrefixOfAux (p s : String) : Pos → Bool
+| i :=
+  if p.atEnd i then true
+  else
+    let c₁ := p.get i in
+    let c₂ := s.get i in
+    c₁ == c₂ && isPrefixOfAux (s.next i)
+
+/- Return true iff `p` is a prefix of `s` -/
+def isPrefixOf (p : String) (s : String) : Bool :=
+p.length ≤ s.length && isPrefixOfAux p s 0
+
 end String
 
 namespace Substring

tests/compiler/str.lean

@@ -18,4 +18,11 @@ IO.println (s₁.extract (b+8) e) *>
 IO.println (toString e) *>
 IO.println (repr "   aaa   ".trim) *>
 showChars s₁.length s₁ 0  *>
+IO.println ("abc".isPrefixOf "abcd") *>
+IO.println ("abcd".isPrefixOf "abcd") *>
+IO.println ("".isPrefixOf "abcd") *>
+IO.println ("".isPrefixOf "") *>
+IO.println ("ab".isPrefixOf "cb") *>
+IO.println ("ab".isPrefixOf "a") *>
+IO.println ("αb".isPrefixOf "αbc") *>
 pure 0

tests/compiler/str.lean.expected.out

@@ -21,3 +21,10 @@ _world_β
 >> d
 >> _
 >> β
+true
+true
+true
+true
+false
+false
+true