chore(library/init/data/string/basic): remove broken lineColumn obs…

…oleted by `FileMap`
leanprover · Sep 19, 2019 · f22c17e · f22c17e
1 parent 8cb387e
commit f22c17e
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 23 deletions.
diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
@@ -257,17 +257,6 @@ def prevn : Iterator → Nat → Iterator
 | it, i+1 => prevn it.prev i
 end Iterator
 
-private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat
-| i, r@(line, col) =>
-  if atEnd s i then r
-  else
-    let c := s.get i;
-    if c = '\n' then lineColumnAux (s.next i) (line+1, 0)
-    else lineColumnAux (s.next i) (line, col+1)
-
-def lineColumn (s : String) (pos : Pos) : Nat × Nat :=
-lineColumnAux s 0 (1, 0)
-
 partial def offsetOfPosAux (s : String) (pos : Pos) : Pos → Nat → Nat
 | i, offset =>
   if i == pos || s.atEnd i then offset

diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean
@@ -7,9 +7,3 @@
 #eval "αβcc".mkIterator.next.next.pos
 #eval "αβcc".mkIterator.next.setCurr 'a'
 #eval "αβcd".mkIterator.toEnd.pos
-#eval "ab\n\nfoo bla".lineColumn 0
-#eval "ab\n\nfoo bla".lineColumn 1
-#eval "ab\n\nfoo bla".lineColumn 2
-#eval "ab\n\nfoo bla".lineColumn 3
-#eval "ab\n\nfoo bla".lineColumn 8
-#eval "ab\n\nfoo bla".lineColumn 100
diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out
@@ -7,9 +7,3 @@
 4
 (String.Iterator.mk "αacc" 2)
 6
-(3, 7)
-(3, 7)
-(3, 7)
-(3, 7)
-(3, 7)
-(3, 7)
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,9 +7,3 @@ @@
     (String.Iterator.mk "αacc" 2)
-    (3, 7)
-    (3, 7)
-    (3, 7)
-    (3, 7)
-    (3, 7)
-    (3, 7)