diff options
| author | Andreas Grois <andi@grois.info> | 2025-04-13 13:22:53 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-04-13 13:22:53 +0200 |
| commit | 8dbe99432db14b5f73585b9e34ecff6e61e76ca8 (patch) | |
| tree | 5661b583c8ba54713ce876add172b64304ec8957 /Day17.lean | |
| parent | 2390fe0a2fbbdd283d21049a1e997026d7d1948c (diff) | |
Lean 4.16
Diffstat (limited to 'Day17.lean')
| -rw-r--r-- | Day17.lean | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -280,8 +280,7 @@ instance : Finite (PathNode heatLossMap) where rewrite (occs := .pos [2]) [←Function.comp_assoc] simp only[Finite.nth_inverse_enumerate, Function.id_comp, PathNode.ofTuple_inv_toTuple] -instance : LeanAStar.AStarNode (PathNode heatLossMap) where - Costs := Nat +instance : LeanAStar.AStarNode (PathNode heatLossMap) Nat where costsLe := Nat.ble costs_order := ⟨BinaryHeap.nat_ble_to_heap_transitive_le, BinaryHeap.nat_ble_to_heap_le_total⟩ remaining_costs_heuristic := PathNode.estimateMinimumCostToGoal |