diff options
Diffstat (limited to 'LeanAStarTest')
| -rw-r--r-- | LeanAStarTest/Tests.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/LeanAStarTest/Tests.lean b/LeanAStarTest/Tests.lean index 1e00803..ca3a825 100644 --- a/LeanAStarTest/Tests.lean +++ b/LeanAStarTest/Tests.lean @@ -81,7 +81,7 @@ instance : GetElem (TwoDArray α) (TwoDArray.Coordinate a) α (λc _ ↦ a = c) a.data[a.valid▸idx] instance : Functor TwoDArray where - map := λf b ↦ {b with data := b.data.map f, valid := (Array.size_map f b.data)▸b.valid} + map := λf b ↦ {b with data := b.data.map f, valid := (Array.size_map (f := f) (xs := b.data))▸b.valid} private theorem TwoDArray.Coordinate.map_size (arr : TwoDArray α) (f : α → β) : (Functor.map f arr).width = arr.width ∧ (Functor.map f arr).height = arr.height := ⟨rfl, rfl⟩ @@ -96,7 +96,7 @@ private def parseTiles (l : String) : Option (TwoDArray Tile) := if h : lines.isEmpty then none else do - let width := String.length $ lines.head (List.isEmpty_eq_false.mp ((Bool.not_eq_true _).mp h)) + let width := String.length $ lines.head (List.isEmpty_eq_false_iff.mp ((Bool.not_eq_true _).mp h)) let height := lines.length -- just convert it all and check validity later. It isn't user input anyhow. let mut result : Array Tile := Array.empty |