From 5224df56a368b8691aea3bcbb7781a16723fd49e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jan 2014 08:36:48 -0800 Subject: [PATCH] test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier Signed-off-by: Leonardo de Moura --- tests/lean/simp7.lean | 10 ++++++++++ tests/lean/simp7.lean.expected.out | 11 +++++++++++ 2 files changed, 21 insertions(+) create mode 100644 tests/lean/simp7.lean create mode 100644 tests/lean/simp7.lean.expected.out diff --git a/tests/lean/simp7.lean b/tests/lean/simp7.lean new file mode 100644 index 000000000..4f0b5fb49 --- /dev/null +++ b/tests/lean/simp7.lean @@ -0,0 +1,10 @@ +variables a b c d e f : Bool +rewrite_set simple +add_rewrite and_assoc and_comm and_left_comm : simple +(* +local t = parse_lean("(f ∧ e) ∧ (d ∧ c) ∧ (b ∧ a)") +local t2 = simplify(t, "simple") +print(t) +print("====>") +print(t2) +*) \ No newline at end of file diff --git a/tests/lean/simp7.lean.expected.out b/tests/lean/simp7.lean.expected.out new file mode 100644 index 000000000..d11e97dba --- /dev/null +++ b/tests/lean/simp7.lean.expected.out @@ -0,0 +1,11 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: c + Assumed: d + Assumed: e + Assumed: f +(f ∧ e) ∧ (d ∧ c) ∧ b ∧ a +====> +a ∧ b ∧ c ∧ d ∧ e ∧ f