From 7d9d89bae6523cea74a64d7661031d32044af580 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 19:49:14 -0800
Subject: [PATCH] test(tests/lean/extra): add test for saving recursive
 equation pre-terms

---
 src/shell/CMakeLists.txt           |  3 +++
 tests/lean/extra/eqn_macro1.lean   | 10 ++++++++++
 tests/lean/extra/eqn_macro2.lean   |  4 ++++
 tests/lean/extra/test_eqn_macro.sh | 10 ++++++++++
 4 files changed, 27 insertions(+)
 create mode 100644 tests/lean/extra/eqn_macro1.lean
 create mode 100644 tests/lean/extra/eqn_macro2.lean
 create mode 100755 tests/lean/extra/test_eqn_macro.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 77131b164..0f401e7c2 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -34,6 +34,9 @@ add_test(lean_unknown_file2 bash ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CM
 add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/consume_args.input")
 add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/options_cmd.trace")
 add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/commands.trace")
+add_test(NAME "lean_eqn_macro"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./test_eqn_macro.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/extra/eqn_macro1.lean b/tests/lean/extra/eqn_macro1.lean
new file mode 100644
index 000000000..2c753a387
--- /dev/null
+++ b/tests/lean/extra/eqn_macro1.lean
@@ -0,0 +1,10 @@
+open nat
+
+notation `foo` a :=
+  match a with
+   (c, d) := c + d
+  end
+
+eval foo (2, 3)
+
+notation `bla` a `with` H := a ↓ H
diff --git a/tests/lean/extra/eqn_macro2.lean b/tests/lean/extra/eqn_macro2.lean
new file mode 100644
index 000000000..3c8ceb716
--- /dev/null
+++ b/tests/lean/extra/eqn_macro2.lean
@@ -0,0 +1,4 @@
+import eqn_macro1
+open nat
+
+eval foo (2, 3)
diff --git a/tests/lean/extra/test_eqn_macro.sh b/tests/lean/extra/test_eqn_macro.sh
new file mode 100755
index 000000000..913559444
--- /dev/null
+++ b/tests/lean/extra/test_eqn_macro.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: test_eq_macro.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export LEAN_PATH=../../../library:.
+$LEAN -o eqn_macro1.olean eqn_macro1.lean
+$LEAN eqn_macro2.lean