diff options
| -rw-r--r-- | LeanAStarTest/Tests.lean | 4 | ||||
| -rw-r--r-- | lakefile.toml | 8 |
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" |