From bb6cbe0fe0c415fee1ece7980b0667055b0ed2db Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 17 Dec 2024 20:00:48 +0100 Subject: Remove useless simp_wf tactic calls --- Day10.lean | 1 - 1 file changed, 1 deletion(-) (limited to 'Day10.lean') 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 _ _ -- cgit v1.2.3