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

chore(tests/lean/run/blast_cc_heq9): make sure that only congruence closure module is used

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-13 22:13:04 -08:00
parent 37fdac4d65
commit 60861d7dea
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/run/blast_cc_heq9.lean
View file

@ -1,4 +1,5 @@
open subtype
set_option blast.strategy "cc"
example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
h = f a → h b = f a b :=