michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/blast_cc1): option name

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 12:23:00 -08:00
parent 6abf2fd975
commit bed03272f5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/blast_cc1.lean
View file

@ -18,7 +18,7 @@ open perm
example (a b c d : list nat) : a ~ b → c ~ b → d ~ c → a ~ d :=
by blast
set_option trace.congruence_closure true
set_option trace.cc true
example (a b c d : list nat) : a ~ b → c ~ b → d = c → a ~ d :=
by blast