refactor: make TProd reducible (#12686)

In various places we want `TProd α (i :: is) = α i × TProd α` to be transparent.
leanprover-community · May 6, 2024 · 3e7a195 · 3e7a195
1 parent b8ee9e3
commit 3e7a195
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Prod/TProd.lean b/Mathlib/Data/Prod/TProd.lean
@@ -44,7 +44,7 @@ namespace List
 variable (α)
 
 /-- The product of a family of types over a list. -/
-def TProd (l : List ι) : Type v :=
+abbrev TProd (l : List ι) : Type v :=
   l.foldr (fun i β => α i × β) PUnit
 #align list.tprod List.TProd