Leonardo de Moura
|
7a24fe73ca
|
chore: remove dead code
|
2020-10-25 20:49:30 -07:00 |
|
Leonardo de Moura
|
2be87ecd92
|
chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false
|
2019-03-21 15:06:44 -07:00 |
|
Leonardo de Moura
|
20ba4c4b04
|
feat(kernel): opaque constants
They are very similar to `theorems`, but they are never ever unfolded.
|
2019-03-15 15:45:06 -07:00 |
|
Leonardo de Moura
|
776c977742
|
refactor(kernel): continue constant_info/declaration refactoring
|
2018-08-27 17:23:26 -07:00 |
|
Leonardo de Moura
|
82095cc018
|
refactor(kernel): split declaration into declaration and constant_info
This is just another step towards the design described at commit 16598391a07d4a
|
2018-08-22 17:53:11 -07:00 |
|
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 |
|