From cc21bfd01d283d52b78eff45232fa90f5abdacd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Jun 2014 09:31:27 -0700
Subject: [PATCH] test(tests/lean/run): more tests on how to deal with
 ambiguity

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/e8.lean | 39 +++++++++++++++++++++++++++++++++++++++
 tests/lean/run/e9.lean | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+)
 create mode 100644 tests/lean/run/e8.lean
 create mode 100644 tests/lean/run/e9.lean

diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
new file mode 100644
index 0000000000..cf7ab93c47
--- /dev/null
+++ b/tests/lean/run/e8.lean
@@ -0,0 +1,39 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+  coercion of_nat
+end
+
+-- Using "only" the notation and declarations from the namespaces nat and int
+using [notation] nat
+using [notation] int
+using [decls] nat
+using [decls] int
+
+variables n m : nat
+variables i j : int
+check n + m
+check i + j
+
+-- The following check does not work, since we are not using the coercions
+-- check n + i
+
+-- Here is a possible trick for this kind of configuration
+definition add_ni (a : nat) (b : int) := (of_nat a) + b
+definition add_in (a : int) (b : nat) := a + (of_nat b)
+infixl + := add_ni
+infixl + := add_in
+
+check i + n
+check n + i
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
new file mode 100644
index 0000000000..01942c2509
--- /dev/null
+++ b/tests/lean/run/e9.lean
@@ -0,0 +1,38 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+end
+
+namespace int_coercions
+  coercion int.of_nat
+end
+
+-- Using "only" the notation and declarations from the namespaces nat and int
+using nat
+using int
+
+variables n m : nat
+variables i j : int
+check n + m
+check i + j
+
+section
+  -- Temporarily use the int_coercions
+  using int_coercions
+  check n + i
+end
+
+-- The following one is an error
+-- check n + i
+