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

test(tests/lean/run/blast_ematch10): make sure the test is for the cc module

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-04 14:03:51 -08:00
parent a8b6a286dd
commit 5d38a5a5cd
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/blast_ematch10.lean
View file

@ -1,4 +1,9 @@
attribute iff [reducible]
set_option blast.subst false
set_option blast.simp false
example (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
by blast
set_option pp.beta true
print lemma1