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

fix(tests/lean/run/blast9): missing option

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-05 19:26:37 -08:00
parent aa998bfad3
commit ae8efb684e
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -5,6 +5,8 @@ set_option blast.strategy "preprocess"
example (p : Prop) (a b c : nat) : [a, b, c] = [] → p :=
by blast
set_option blast.strategy "simple"
lemma l1 (a b c d e f : nat) : [a, b, c] = [d, e, f] → a = d ∧ b = e ∧ c = f :=
by blast