test(tests/lean): add test showing that the binder type update should not change the parameter order

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

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