test(tests/lean): add test disabling contextual simplifications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/simp15.lean

@@ -0,0 +1,17 @@
+rewrite_set simple
+add_rewrite and_truer and_truel and_falser and_falsel or_falsel : simple
+(*
+  add_congr_theorem("simple", "and_congr")
+  add_congr_theorem("simple", "or_congr")
+*)
+
+variables a b c : Nat
+
+(*
+local opts = options({"simplifier", "contextual"}, false)
+local t = parse_lean([[a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)]])
+local s, pr = simplify(t, "simple", get_environment(), context(), opts)
+print(s)
+print(pr)
+print(get_environment():type_check(pr))
+*)

tests/lean/simp15.lean.expected.out

@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)
+refl (a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a))
+(a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)) = (a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a))