From 3bb53810c5e286cf60c32e4d4dad5ee6f00d618b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Jun 2014 09:48:47 -0700
Subject: [PATCH] test(lean/run): add notation test

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

diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean
new file mode 100644
index 0000000000..00b4d832f9
--- /dev/null
+++ b/tests/lean/run/n4.lean
@@ -0,0 +1,20 @@
+definition [inline] Bool : Type.{1} := Type.{0}
+section
+  variable N : Type.{1}
+  variables a b c : N
+  variable and : Bool → Bool → Bool
+  infixr `∧` 35 := and
+  variable le : N → N → Bool
+  variable lt : N → N → Bool
+  precedence `≤`:50
+  precedence `<`:50
+  infixl ≤ := le
+  infixl < := lt
+  check a ≤ b
+  definition T : Bool := a ≤ b
+  check T
+end
+check T
+(*
+print(get_env():find("T"):value())
+*)
\ No newline at end of file