summaryrefslogtreecommitdiff
path: root/Day10.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-12-17 20:00:48 +0100
committerAndreas Grois <andi@grois.info>2024-12-17 20:00:48 +0100
commitbb6cbe0fe0c415fee1ece7980b0667055b0ed2db (patch)
tree846b0d59555affa540000b6b84db02629f8cac00 /Day10.lean
parent19d4b4e41a967c0c8b3329cd1c4a0617178c5a94 (diff)
Remove useless simp_wf tactic callsHEADmain
Diffstat (limited to 'Day10.lean')
-rw-r--r--Day10.lean1
1 files changed, 0 insertions, 1 deletions
diff --git a/Day10.lean b/Day10.lean
index 720b7b9..c746ed1 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -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 _ _