style: pp_with_univ for TypeVec & PFunctor & MvPFunctor (#7742)

leanprover-community · Oct 18, 2023 · 68b12e1 · 68b12e1
1 parent 5cff8eb
commit 68b12e1
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/Mathlib/Data/PFunctor/Multivariate/Basic.lean b/Mathlib/Data/PFunctor/Multivariate/Basic.lean
@@ -24,6 +24,7 @@ open MvFunctor
 
 /-- multivariate polynomial functors
 -/
+@[pp_with_univ]
 structure MvPFunctor (n : ℕ) where
   /-- The head type -/
   A : Type u

diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean
@@ -27,6 +27,7 @@ An element of `P.obj α` is a pair `⟨a, f⟩`, where `a` is an element of a ty
 `f : B a → α`. Think of `a` as the shape of the object and `f` as an index to the relevant
 elements of `α`.
 -/
+@[pp_with_univ]
 structure PFunctor where
   /-- The head type -/
   A : Type u

diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
@@ -35,6 +35,7 @@ to it, we need support functions and lemmas to mediate between constructions.
 universe u v w
 
 /-- n-tuples of types, as a category -/
+@[pp_with_univ]
 def TypeVec (n : ℕ) :=
   Fin2 n → Type*
 #align typevec TypeVec