diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 287bce06ef..358321006e 100644 --- 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 index 1b69c503d3..2d840ef558 100644 --- 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 index bf4bf5bcf2..53ed150410 100644 --- 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)