test(tests/lean): add tests for simp priorities

tests/lean/simplifier20.lean

@@ -0,0 +1,31 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority 30000]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- c
+
+attribute H2 [simp] [priority 20000]
+attribute H1 [simp] [priority 20001]
+
+#simplify eq env 0 a -- b
+
+end test_congr

tests/lean/simplifier20.lean.expected.out

@@ -0,0 +1,5 @@
+c
+b
+c
+c
+b

tests/lean/simplifier21.lean

@@ -0,0 +1,28 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H1 [simp] [priority std.priority.default+1]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority std.priority.default+2]
+attribute H1 [simp] [priority std.priority.default+1]
+
+#simplify eq env 0 a -- c
+
+end test_congr

tests/lean/simplifier21.lean.expected.out

@@ -0,0 +1,4 @@
+c
+b
+b
+c