Leonardo de Moura
|
487a1e7f89
|
refactor(kernel): remove extension_context
We replaced it with abstract_type_context
|
2016-03-19 15:15:39 -07:00 |
|
Leonardo de Moura
|
e7f1f409c4
|
refactor(kernel): simplify kernel type_checker
TODO: cleanup, move justification/metavar/constraints to library
|
2016-03-18 16:28:42 -07:00 |
|
Leonardo de Moura
|
3c878ecd01
|
feat(kernel): add let-expressions to the kernel
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
|
2016-02-29 16:40:17 -08:00 |
|
Leonardo de Moura
|
061e26157e
|
fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking
|
2015-05-08 12:41:23 -07:00 |
|
Leonardo de Moura
|
92c424936a
|
refactor(kernel/macro_definition_cell): improve macro get_type API
|
2014-10-07 16:38:31 -07:00 |
|
Leonardo de Moura
|
b6781711b1
|
refactor(*): explicit initialization/finalization for serialization
modules, expression annotations, and tactics
|
2014-09-22 15:26:41 -07:00 |
|
Leonardo de Moura
|
b9489ce585
|
fix(frontends/let): let-expression pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-29 10:58:27 -07:00 |
|
Leonardo de Moura
|
be56fcf0bd
|
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-28 18:20:58 -07:00 |
|