Fix testsHEADmain

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