From 1658be20f1679d38569c1a9f693598581fd480f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Jun 2019 14:16:45 -0700
Subject: [PATCH] feat(library/init/data/string): add `String.isPrefixOf`

---
 library/init/data/string/basic.lean  | 12 ++++++++++++
 tests/compiler/str.lean              |  7 +++++++
 tests/compiler/str.lean.expected.out |  7 +++++++
 3 files changed, 26 insertions(+)

diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index 63c056d7fc..dde6d333e3 100644
--- a/library/init/data/string/basic.lean
+++ b/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
diff --git a/tests/compiler/str.lean b/tests/compiler/str.lean
index a635a7c345..5abe86f525 100644
--- a/tests/compiler/str.lean
+++ b/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
diff --git a/tests/compiler/str.lean.expected.out b/tests/compiler/str.lean.expected.out
index cce88cb562..89847d6c72 100644
--- a/tests/compiler/str.lean.expected.out
+++ b/tests/compiler/str.lean.expected.out
@@ -21,3 +21,10 @@ _world_β
 >> d
 >> _
 >> β
+true
+true
+true
+true
+false
+false
+true