Leonardo de Moura
|
95487f9985
|
feat(library/aux_definition): add mk_aux_lemma
|
2016-09-06 08:57:04 -07:00 |
|
Leonardo de Moura
|
f7df7dc9a7
|
refactor(kernel): add reducibility_hints
|
2016-09-04 16:30:02 -07:00 |
|
Leonardo de Moura
|
2fc0e5fa05
|
feat(library/equations_compiler/structural_rec): add aux definition
|
2016-08-30 18:33:24 -07:00 |
|
Leonardo de Moura
|
a93eada058
|
feat(library/type_context): improved (and simplified) cache management for type_context
|
2016-08-23 17:56:58 -07:00 |
|
Leonardo de Moura
|
3de9509644
|
feat(library/aux_definition): add helper functions for creating auxiliary definitions
|
2016-08-22 17:59:40 -07:00 |
|