test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
913d893204
commit
5224df56a3
2 changed files with 21 additions and 0 deletions
10
tests/lean/simp7.lean
Normal file
10
tests/lean/simp7.lean
Normal file
|
@ -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)
|
||||||
|
*)
|
11
tests/lean/simp7.lean.expected.out
Normal file
11
tests/lean/simp7.lean.expected.out
Normal file
|
@ -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
|
Loading…
Reference in a new issue