From 349cdb3fe74aa688193dbd5c6ff0af7c2bea7a68 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Apr 2015 13:04:05 -0700
Subject: [PATCH] test(tests/lean): add test showing that the binder type
 update should not change the parameter order

---
 tests/lean/param_binder_update2.lean          | 23 +++++++++++++++++++
 .../param_binder_update2.lean.expected.out    |  4 ++++
 2 files changed, 27 insertions(+)
 create mode 100644 tests/lean/param_binder_update2.lean
 create mode 100644 tests/lean/param_binder_update2.lean.expected.out

diff --git a/tests/lean/param_binder_update2.lean b/tests/lean/param_binder_update2.lean
new file mode 100644
index 000000000..862c293e9
--- /dev/null
+++ b/tests/lean/param_binder_update2.lean
@@ -0,0 +1,23 @@
+section
+  parameters {A : Type} {B : Type}
+
+  definition foo1 (a : A) (b : B) := a
+
+  parameters (B) {A} -- Should not change the order of the parameters
+
+  definition foo2 (a : A) (b : B) := a
+
+  parameters {B} (A)
+
+  definition foo3 (a : A) (b : B) := a
+
+  parameters (A) (B)
+
+  definition foo4 (a : A) (b : B) := a
+
+end
+
+check @foo1
+check @foo2
+check @foo3
+check @foo4
diff --git a/tests/lean/param_binder_update2.lean.expected.out b/tests/lean/param_binder_update2.lean.expected.out
new file mode 100644
index 000000000..b5b750ee7
--- /dev/null
+++ b/tests/lean/param_binder_update2.lean.expected.out
@@ -0,0 +1,4 @@
+foo1 : Π {A : Type} {B : Type}, A → B → A
+foo2 : Π {A : Type} (B : Type), A → B → A
+foo3 : Π (A : Type) {B : Type}, A → B → A
+foo4 : Π (A : Type) (B : Type), A → B → A