summaryrefslogtreecommitdiff
path: root/Common/Parsing.lean
diff options
context:
space:
mode:
Diffstat (limited to 'Common/Parsing.lean')
-rw-r--r--Common/Parsing.lean1
1 files changed, 0 insertions, 1 deletions
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 348db25..637f807 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -103,7 +103,6 @@ protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except
RectangularGrid.parseSingleLine parseCharacter (alreadyParsed.push element) (remainingLine.drop 1)
termination_by remainingLine.bsize
decreasing_by
- simp_wf
simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁
simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq]
split