Leonardo de Moura
|
713c97a3be
|
fix(library/compiler/preprocess): make sure no_confusion is not expanded by expand_aux
|
2016-05-25 17:57:17 -07:00 |
|
Leonardo de Moura
|
abd2bbab78
|
feat(library/compiler/preprocess): expand auxiliary declarations automatically created by Lean (e.g., transitivite instances)
These declarations do not have VM bytecode associated with them.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2016-05-25 17:09:16 -07:00 |
|
Leonardo de Moura
|
752c81a166
|
fix(library/compiler/nat_value): add expand method, otherwise we may fail to type check terms using nat_value_macro
|
2016-05-13 12:50:28 -07:00 |
|
Leonardo de Moura
|
df9352ea6e
|
feat(library/compiler): better support for numeric constants
|
2016-05-12 16:33:37 -07:00 |
|
Leonardo de Moura
|
f2af5828ba
|
refactor(library/compiler): preprocess_rec ==> preprocess
|
2016-05-12 16:03:39 -07:00 |
|