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