diff options
| -rw-r--r-- | Common/Parsing.lean | 1 | ||||
| -rw-r--r-- | Day10.lean | 1 | ||||
| -rw-r--r-- | Day12.lean | 1 |
3 files changed, 0 insertions, 3 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 @@ -1007,7 +1007,6 @@ private def removePathsMet {area : Area} : (List $ Area.PathHead area) → (List termination_by x => x.length decreasing_by all_goals - simp_wf exact Nat.lt_succ.mpr $ List.listFilterSmallerOrEqualList _ _ @@ -72,7 +72,6 @@ where | .ok v => parseLeftBlock (s.drop 1) $ v :: p termination_by s => s.bsize decreasing_by - simp_wf rename_i h₁ apply Substring.drop_bsize_dec _ _ h₁ Nat.one_ne_zero parseMaskChar : Char → Except ParsingError SpringState := λ |