Fix testsHEADmain

2 files changed, 8 insertions, 4 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
diff --git a/lakefile.toml b/lakefile.toml
index 91e4800..85a03a9 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,14 +1,18 @@
 name = "lean-astar"
 version = "0.1.0"
 defaultTargets = ["LeanAStar"]
-testDriver = "LeanAStarTest"
+testDriver = "leanastartest"
 
 [[lean_lib]]
 name = "LeanAStar"
 
-[[lean_exe]]
+[[lean_lib]]
 name = "LeanAStarTest"
 
+[[lean_exe]]
+name = "leanastartest"
+root = "LeanAStarTest"
+
 [[require]]
 name = "BinaryHeap"
 git = "http://git.grois.info/BinaryHeap"