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 /Day10.lean | |
| parent | 19d4b4e41a967c0c8b3329cd1c4a0617178c5a94 (diff) | |
Diffstat (limited to 'Day10.lean')
| -rw-r--r-- | Day10.lean | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -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 _ _ |
