From dc5553ea5c34df8c9612cb29bf352702eed33fab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Jun 2014 09:12:27 -0700
Subject: [PATCH] test(tests/lean/run): add test demonstrating how to control
 ambiguity

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/e7.lean | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 tests/lean/run/e7.lean

diff --git a/tests/lean/run/e7.lean b/tests/lean/run/e7.lean
new file mode 100644
index 000000000..013cfa5a0
--- /dev/null
+++ b/tests/lean/run/e7.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 nat
+using int
+
+variables n m : nat
+variables i j : int
+
+-- 'Most recent' are always tried first
+print raw i + n
+-- So, in the following one int.add is tried first, and we
+-- get int.add (int.of_nat n) (int.of_nat m)
+check n + m
+
+print ">>> Forcing nat notation"
+-- Force natural numbers
+check #nat n + m
+
+-- Moving 'nat' to the 'front'
+print ">>> Moving nat notation to the 'front'"
+using nat
+print raw i + n
+check n + m