From 3e92cd49223c28c90e76a0be468c1d0ab0266962 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 1 Feb 2015 11:39:47 -0500
Subject: [PATCH] feat(library/data,init/prod,sigma,sum): make more notation
 available at top level

---
 library/data/prod.lean  |  1 -
 library/data/sigma.lean | 12 +++++++++---
 library/data/sum.lean   |  5 +++--
 library/init/prod.lean  |  7 ++++++-
 library/init/sigma.lean |  4 ++++
 5 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/library/data/prod.lean b/library/data/prod.lean
index c1e5e5a7c..340bfdc80 100644
--- a/library/data/prod.lean
+++ b/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
 
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index c8c095b99..f4c3eed2f 100644
--- a/library/data/sigma.lean
+++ b/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
 
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 3296b87ac..d8b8eed74 100644
--- a/library/data/sum.lean
+++ b/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
diff --git a/library/init/prod.lean b/library/init/prod.lean
index ef2381b64..4e11d8d6f 100644
--- a/library/init/prod.lean
+++ b/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
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index ede5fa4c9..dbc1d8a6f 100644
--- a/library/init/sigma.lean
+++ b/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