Apply suggestions from code review

alexkeizer · Dec 4, 2024 · 2585928 · 2585928
1 parent 9cfc50c
commit 2585928
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -13,8 +13,8 @@ namespace Prod
 
 open PFin2 (fz fs)
 
-def P : MvPFunctor.{u} 2
-  := .mk PUnit fun _ _ => PFin2 1
+def P : MvPFunctor.{u} 2 := 
+  .mk PUnit fun _ _ => PFin2 1
 
 
 abbrev QpfProd' := P.Obj
@@ -30,8 +30,8 @@ abbrev Prod' : TypeFun 2
 /--
   Constructor for `QpfProd'`
 -/
-def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ
-  := ⟨
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := 
+  ⟨
       ⟨⟩,
       fun
       | 1, _ => a