feat(library/data,init/prod,sigma,sum): make more notation available at top level

library/data/prod.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.prod
 Author: Leonardo de Moura, Jeremy Avigad
 -/
-
 import logic.eq
 open inhabited decidable eq.ops
 

library/data/sigma.lean

@@ -1,6 +1,12 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.sigma
+Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
+
+Sigma types, aka dependent sum.
+-/
 import logic.cast
 open inhabited eq.ops sigma.ops
 

library/data/sum.lean

@@ -10,9 +10,10 @@ The sum type, aka disjoint union.
 import logic.connectives
 open inhabited eq.ops
 
+notation A ⊎ B := sum A B
+notation A + B := sum A B
+
 namespace sum
-  notation A ⊎ B := sum A B
-  notation A + B := sum A B
   namespace low_precedence_plus
     reserve infixr `+`:25  -- conflicts with notation for addition
     infixr `+` := sum

library/init/prod.lean

@@ -6,7 +6,7 @@ Module: init.prod
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
-import init.wf
+import init.num init.wf
 
 definition pair := @prod.mk
 
@@ -24,6 +24,11 @@ namespace prod
   -- notation for n-ary tuples
   notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
 
+  namespace ops
+  postfix `.1`:(max+1) := pr1
+  postfix `.2`:(max+1) := pr2
+  end ops
+
   open well_founded
 
   section

library/init/sigma.lean

@@ -11,6 +11,10 @@ import init.num init.wf init.logic init.tactic
 structure sigma {A : Type} (B : A → Type) :=
 mk :: (pr1 : A) (pr2 : B pr1)
 
+definition dpair := @sigma.mk
+definition dpr1 := @sigma.pr1
+definition dpr2 := @sigma.pr2
+
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
 namespace sigma