From d30f387e72c5856d624023952d6a181a08521e72 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Jul 2014 14:48:19 -0700
Subject: [PATCH] feat(library/standard): add namespace 'pair'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/pair.lean | 5 ++++-
 tests/lean/run/class1.lean | 1 +
 tests/lean/run/class2.lean | 1 +
 tests/lean/run/class3.lean | 1 +
 tests/lean/run/class6.lean | 1 +
 tests/lean/run/ptst.lean   | 1 +
 6 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/library/standard/pair.lean b/library/standard/pair.lean
index 0282406f7..e46243b7c 100644
--- a/library/standard/pair.lean
+++ b/library/standard/pair.lean
@@ -3,6 +3,7 @@
 -- Author: Leonardo de Moura
 import logic
 
+namespace pair
 inductive pair (A : Type) (B : Type) : Type :=
 | mk_pair : A → B → pair A B
 
@@ -25,10 +26,12 @@ section
   theorem pair_ext (p : pair A B) : mk_pair (fst p) (snd p) = p
   := pair_rec (λ x y, refl (mk_pair x y)) p
 end
-instance pair_inhabited
+
+instance pair.pair_inhabited
 
 precedence `×`:30
 infixr × := pair
 
 -- notation for n-ary tuples
 notation `(` h `,` t:(foldl `,` (e r, mk_pair r e) h) `)` := t
+end
\ No newline at end of file
diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index 735e7d984..3d1eacb71 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,5 +1,6 @@
 import standard
 using num
+using pair
 
 definition H : inhabited (Bool × num × (num → num)) := _
 
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index e6c00e2ce..53945b678 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,5 +1,6 @@
 import standard
 using num
+using pair
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Bool × A × (B → num))
 := _
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 6f35c3b16..767ddb9ae 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -1,5 +1,6 @@
 import standard
 using num
+using pair
 
 section
   parameter {A : Type}
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index eb73039e1..9897342e8 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -1,4 +1,5 @@
 import standard
+using pair
 
 inductive t1 : Type :=
 | mk1 : t1
diff --git a/tests/lean/run/ptst.lean b/tests/lean/run/ptst.lean
index e3e486cf9..d5a427de3 100644
--- a/tests/lean/run/ptst.lean
+++ b/tests/lean/run/ptst.lean
@@ -1,4 +1,5 @@
 import standard
+using pair
 
 -- Test tuple notation
 check (3, false, 1, true)