diff options
| author | Andreas Grois <andi@grois.info> | 2024-12-17 20:00:48 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-12-17 20:00:48 +0100 |
| commit | bb6cbe0fe0c415fee1ece7980b0667055b0ed2db (patch) | |
| tree | 846b0d59555affa540000b6b84db02629f8cac00 /Common/Parsing.lean | |
| parent | 19d4b4e41a967c0c8b3329cd1c4a0617178c5a94 (diff) | |
Diffstat (limited to 'Common/Parsing.lean')
| -rw-r--r-- | Common/Parsing.lean | 1 |
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 |