From 79e561bb05230c7e97f7e75723bf13a03e6bb9ab Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Wed, 19 Nov 2025 22:49:06 +0100 Subject: Fix tests --- LeanAStarTest/Tests.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'LeanAStarTest') 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 -- cgit v1.2.3