Leonardo de Moura
|
ec1aa2553c
|
refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object
TODO: inductive, constructor, recursor
|
2018-06-25 10:05:45 -07:00 |
|
Leonardo de Moura
|
c0e1d05199
|
chore(kernel): type_checker ==> old_type_checker
|
2018-06-06 16:10:40 -07:00 |
|
Leonardo de Moura
|
c9a6f98454
|
chore(library/sorry): style
|
2018-05-29 22:27:03 -07:00 |
|
Leonardo de Moura
|
1332fbabd6
|
feat(library,frontends): remove sorry macro
Lean4 will not have macros.
|
2018-05-24 14:00:30 -07:00 |
|
Gabriel Ebner
|
00ac867ddf
|
feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys
|
2017-05-23 11:14:30 -07:00 |
|
diakopter
|
55b9f3e690
|
chore(library): clang warnings - missing override
|
2017-02-06 13:44:20 -08:00 |
|
Gabriel Ebner
|
95068e4e79
|
feat(library/sorry): make sorry a macro
|
2017-02-05 14:01:03 +01:00 |
|
Leonardo de Moura
|
5a48a2cebe
|
feat(library/app_builder): add mk_sorry method
|
2015-11-08 14:05:02 -08:00 |
|
Leonardo de Moura
|
bf081ed431
|
refactor(kernel): rename var_decl to constant_assumption
Motivation: it matches the notation used to declare it.
|
2014-10-02 17:55:34 -07:00 |
|
Leonardo de Moura
|
2730e5163e
|
feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message
See new test for explanation.
|
2014-09-30 18:04:04 -07:00 |
|
Leonardo de Moura
|
4dd7abb14e
|
refactor(library): explicit initialization/finalization
|
2014-09-23 10:45:14 -07:00 |
|
Leonardo de Moura
|
9a4472cff5
|
fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-29 14:32:53 -07:00 |
|
Leonardo de Moura
|
3d8477f7de
|
fix(library/module): ignore multiple declarations of 'sorry', fixes #59
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-17 15:55:58 -07:00 |
|