From 4eafd201f65e7aa02ec09d25690b5b0096c2303e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Dec 2016 21:35:26 -0800 Subject: [PATCH] test(tests/lean/run): add cc+ac sanity test --- tests/lean/run/cc_ac_support.lean | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 tests/lean/run/cc_ac_support.lean diff --git a/tests/lean/run/cc_ac_support.lean b/tests/lean/run/cc_ac_support.lean new file mode 100644 index 0000000000..fcbef5aef0 --- /dev/null +++ b/tests/lean/run/cc_ac_support.lean @@ -0,0 +1,7 @@ +open tactic + +example (a b c : nat) (f : nat → nat) : f (a + b + c) = f (c + b + a) := +by cc + +example (a b c : nat) (f : nat → nat) : a + b = c → f (c + c) = f (a + b + c) := +by cc