From 0f2172fab54e4e95a7ea7d9ea64e546eea46b4e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Nov 2019 20:02:41 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/mvar3.lean              | 18 ++++++++++++------
 tests/lean/mvar3.lean.expected.out |  4 ++--
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index 881b209a60..eaae5e100d 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -58,8 +58,14 @@ match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x
 def e1    := R1.2.2
 def mctx5 := R1.1
 
-#eval toString $ mctx5.decls.toList.map Prod.fst
-#eval toString mctx5.eAssignment.toList
+def sortNames (xs : List Name) : List Name :=
+(xs.toArray.qsort Name.lt).toList
+
+def sortNamePairs {α} [Inhabited α] (xs : List (Name × α)) : List (Name × α) :=
+(xs.toArray.qsort (fun a b => Name.lt a.1 b.1)).toList
+
+#eval toString $ sortNames $ mctx5.decls.toList.map Prod.fst
+#eval toString $ sortNamePairs $ mctx5.eAssignment.toList
 #eval e1
 #eval check (!e1.hasFVar)
 
@@ -70,10 +76,10 @@ match mkLambdaTest mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3,
 def e2    := R2.2.2
 def mctx6 := R2.1
 
-#eval toString $ mctx6.decls.toList.map Prod.fst
-#eval toString mctx6.eAssignment.toList
+#eval toString $ sortNames $ mctx6.decls.toList.map Prod.fst
+#eval toString $ sortNamePairs $ mctx6.eAssignment.toList
 -- ?n.2 was delayed assigned because ?m.3 is synthetic
-#eval toString $ mctx6.dAssignment.toList.map Prod.fst
+#eval toString $ sortNames $ mctx6.dAssignment.toList.map Prod.fst
 #eval e2
 
 #print "assigning ?m1 and ?n.1"
@@ -87,4 +93,4 @@ def mctx7 := R3.2
 #eval e3
 -- The delayed assignment became a regular one.
 #eval mctx7.getExprAssignment (mkNameNum `n 2)
-#eval toString $ mctx7.dAssignment.toList.map Prod.fst
+#eval toString $ sortNames $ mctx7.dAssignment.toList.map Prod.fst
diff --git a/tests/lean/mvar3.lean.expected.out b/tests/lean/mvar3.lean.expected.out
index 968af7dce0..232edeb19c 100644
--- a/tests/lean/mvar3.lean.expected.out
+++ b/tests/lean/mvar3.lean.expected.out
@@ -1,8 +1,8 @@
-"[m1, m2, n.1, n.2, m3, n.3]"
+"[n.1, n.2, n.3, m1, m2, m3]"
 "[(m1, ?n.1 α), (m2, ?n.3 α x), (m3, ?n.2 α x)]"
 fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) x
 
-"[m1, m2, n.1, n.2, m3, n.3]"
+"[n.1, n.2, n.3, m1, m2, m3]"
 "[(m1, ?n.1 α), (m2, ?n.3 α x)]"
 "[n.2]"
 fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) y