Leonardo de Moura
|
add5266df7
|
fix(frontends/lean, library/tactic): error position in auto quoted terms
This commit also gets rid of the redundant "elaborator failed" error
message.
|
2017-02-09 18:03:04 -08:00 |
|
Leonardo de Moura
|
ceeebb7e40
|
feat(frontends/lean/elaborator): improve error messages for eliminators
|
2016-09-29 11:29:59 -07:00 |
|
Leonardo de Moura
|
7a92ce38bd
|
refactor(frontends/lean): elaborator_exception ==> old_elaborator_exception
|
2016-07-26 16:24:28 -07:00 |
|
Leonardo de Moura
|
461b5f289c
|
feat(frontends/lean/elaborator): new elaborator skeleton
|
2016-07-23 19:02:17 -07:00 |
|
Leonardo de Moura
|
8939351903
|
refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception
|
2014-12-15 19:22:17 -08:00 |
|
Leonardo de Moura
|
498b2f681e
|
feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution
|
2014-10-30 14:44:58 -07:00 |
|
Leonardo de Moura
|
71ccec5b9e
|
refactor(frontends/lean/elaborator): delete old_elaborator, and create frontend_elaborator class that will be based on library/elaborator/elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-10-24 10:45:59 -07:00 |
|
Leonardo de Moura
|
1548ffabb1
|
feat(elaborator): add new elaborator interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-10-22 08:15:36 -07:00 |
|
Soonho Kong
|
5c3866cd71
|
Use fullpath in #include directives, add missing STL headers
|
2013-09-13 03:35:29 -07:00 |
|
Leonardo de Moura
|
4c19cc6957
|
Rename lean frontend files. The prefix lean_ is not necessary anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-12 20:09:35 -07:00 |
|