max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/lean/run): add cc+ac sanity test

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-28 21:35:26 -08:00
parent 9065cf0350
commit 4eafd201f6
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/cc_ac_support.lean Normal file
View file

@ -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