refactor(data/sigma): move notation from sigma.thms to sigma.decl

library/data/sigma/decl.lean

@@ -7,3 +7,15 @@ structure sigma {A : Type} (B : A → Type) :=
 dpair :: (dpr1 : A) (dpr2 : B dpr1)
 
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
+
+namespace sigma
+
+  notation `dpr₁` := dpr1
+  notation `dpr₂` := dpr2
+
+  namespace ops
+  postfix `.1`:10000 := dpr1
+  postfix `.2`:10000 := dpr2
+  notation `⟨` t:(foldr `,`:0 (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
+  end ops
+end sigma

library/data/sigma/thms.lean

@@ -2,24 +2,13 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 import data.sigma.decl
-open inhabited eq.ops
+open inhabited eq.ops sigma.ops
 
 namespace sigma
-
-  notation `dpr₁` := dpr1
-  notation `dpr₂` := dpr2
-
-  namespace ops
-  postfix `.1`:10000 := dpr1
-  postfix `.2`:10000 := dpr2
-  notation `(` t:(foldr `;`:0 (e r, sigma.dpair e r)) `)` := t
-  end ops
-
-  open ops
   universe variables u v
   variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
 
-  definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ( u.1 ; u.2)) : C u :=
+  definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ⟨u.1 , u.2⟩) : C u :=
   destruct u (λx y H, H) H
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
@@ -48,8 +37,8 @@ namespace sigma
 
   variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
 
-  definition dtrip (a : A) (b : B a) (c : C a b) := (a; b; c)
-  definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := (a; b; c; d)
+  definition dtrip (a : A) (b : B a) (c : C a b) := ⟨a, b, c⟩
+  definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := ⟨a, b, c, d⟩
 
   definition dpr1' (x : Σ a, B a) := x.1
   definition dpr2' (x : Σ a b, C a b) := x.2.1
@@ -59,12 +48,12 @@ namespace sigma
 
   theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
       (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
-    (a₁; b₁; c₁) = (a₂; b₂; c₂) :=
+    ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
   dcongr_arg3 dtrip H₁ H₂ H₃
 
   theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
       {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
-      (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : (a₁; b₁; c₁) = (a₂; b₂; c₂) :=
+      (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
   hdcongr_arg3 dtrip H₁ (heq.from_eq H₂) H₃
 
   theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :