Leonardo de Moura
|
9c069a3eda
|
refactor(library/tactic/congruence): rename directory to smt
|
2016-12-30 13:15:19 -08:00 |
|
Leonardo de Moura
|
9065cf0350
|
feat(library/tactic/congruence/theory_ac): add internalization, interface with congruence closure module, and trivial/simp/orient transitions
Still missing: superpose, collapse and compose transitions.
|
2016-12-28 21:35:16 -08:00 |
|
Leonardo de Moura
|
1d519e4c7b
|
feat(library/tactic/congruence): add theory AC skeleton
|
2016-12-27 21:38:03 -08:00 |
|
Leonardo de Moura
|
9e46818563
|
feat(library/tactic/congruence): ematching
|
2016-12-26 15:52:18 -08:00 |
|
Leonardo de Moura
|
6a5f6a84cd
|
feat(library/tactic/congruence/hinst_lemma): add heuristic instantiation lemmas
|
2016-12-25 20:11:58 -08:00 |
|
Leonardo de Moura
|
f777aafa4e
|
feat(library/init/meta,library/tactic/congruence): add congruence closure lean API
|
2016-12-22 16:26:17 -08:00 |
|
Leonardo de Moura
|
d16a3df7a3
|
feat(library/tactic/congruence): initialization and pretty printing
|
2016-12-22 15:18:52 -08:00 |
|