fix leanprover/lean4#6558 build by working around leanprover/lean4#6570

leanprover-community · Jan 9, 2025 · 5899f45 · 5899f45
1 parent c2cc119
commit 5899f45
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/MathlibTest/congr.lean b/MathlibTest/congr.lean
@@ -177,8 +177,8 @@ inductive walk (α : Type) : α → α → Type
   | nil (n : α) : walk α n n
 
 def walk.map (f : α → β) (w : walk α x y) : walk β (f x) (f y) :=
-  match x, y, w with
-  | _, _, .nil n => .nil (f n)
+  match w with
+  | nil x => nil (f x)
 
 example (w : walk α x y) (w' : walk α x' y') (f : α → β) : HEq (w.map f) (w'.map f) := by
   congr!