Leonardo de Moura
|
19bfbe2df8
|
fix(library/blast/congruence_closure): uselist initialization (aka add_occurrence)
Make sure it matches the description in the paper.
|
2016-01-16 19:53:36 -08:00 |
|
Leonardo de Moura
|
60861d7dea
|
chore(tests/lean/run/blast_cc_heq9): make sure that only congruence closure module is used
|
2016-01-13 22:13:04 -08:00 |
|
Leonardo de Moura
|
37fdac4d65
|
test(tests/lean/run/blast_cc_heq9): add new test
|
2016-01-13 22:10:15 -08:00 |
|
Leonardo de Moura
|
3f7122ce07
|
feat(library/blast/congruence_closure): more general congruence lemmas
|
2016-01-13 21:44:32 -08:00 |
|