formatting of Sum.lean

alexkeizer · Dec 18, 2024 · 583858e · 583858e
1 parent ea0cde1
commit 583858e
Showing 1 changed file with 15 additions and 19 deletions.
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
@@ -12,29 +12,25 @@ namespace Sum
 
 universe u
 
-def SumPFunctor : MvPFunctor.{u} 2
-  := ⟨PFin2 2,
-      fun
-      | 0 => !![PFin2 1, PFin2 0] -- inl
-      | 1 => !![PFin2 0, PFin2 1] -- inr
-    ⟩
-
+def SumPFunctor : MvPFunctor.{u} 2 :=
+  ⟨PFin2 2, fun
+    | 0 => !![PFin2 1, PFin2 0] -- inl
+    | 1 => !![PFin2 0, PFin2 1] -- inr
+  ⟩
 
 abbrev QpfSum' := SumPFunctor.Obj
 abbrev QpfSum  := TypeFun.curried QpfSum'
 
-def inl {Γ : TypeVec 2} (a : Γ 1) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 0,
-      fun
-      | 1, _ => a
-    ⟩
-
-def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 1,
-      fun
-      | 0, _ => b
-      | 1, x => by cases x
-    ⟩
+def inl {Γ : TypeVec 2} (a : Γ 1) : QpfSum' Γ :=
+  ⟨PFin2.ofNat' 0, fun
+    | 1, _ => a
+  ⟩
+
+def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ :=
+  ⟨PFin2.ofNat' 1, fun
+    | 0, _ => b
+    | 1, (x : PFin2 _) => by cases x
+  ⟩
 
 
 def Sum' := @TypeFun.ofCurried 2 Sum