Leonardo de Moura
|
91994ff823
|
feat(frontends/lean/elaborator): switch to new let-decls
|
2016-09-10 13:00:53 -07:00 |
|
Leonardo de Moura
|
c25ac7f54f
|
feat(library/equations_compiler): pull nested recursive calls
|
2016-09-09 17:56:56 -07:00 |
|
Leonardo de Moura
|
fc0230730d
|
feat(frontends/lean/elaborator): make sure all equations have the same number of patterns
|
2016-09-09 12:13:41 -07:00 |
|
Leonardo de Moura
|
89bc55aece
|
feat(frontends/lean/elaborator): improve expected type for equation rhs
|
2016-09-08 19:22:26 -07:00 |
|
Leonardo de Moura
|
23e443ef71
|
feat(frontends/lean/elaborator): add support for no_confusion in the new elaborator
|
2016-09-08 18:48:48 -07:00 |
|
Leonardo de Moura
|
b12fa5c8da
|
feat(frontends/lean): add support for 'suffices'-expression in the new elaborator
|
2016-09-08 17:26:27 -07:00 |
|
Leonardo de Moura
|
5c7150c813
|
fix(frontends/lean/elaborator): make sure equations do not contain unassigned metavars before using eqn compiler
|
2016-09-08 10:47:15 -07:00 |
|
Leonardo de Moura
|
31de40ff4d
|
refactor(frontends/lean): rename attribute [constructor] ==> [elab_with_expected_type]
|
2016-09-06 13:12:51 -07:00 |
|
Leonardo de Moura
|
2a912c2650
|
feat(frontends/lean, library): move constructor attribute to frontend
Now, it only affects the elaborator.
|
2016-09-05 09:34:45 -07:00 |
|
Leonardo de Moura
|
3bc5cf8d0e
|
feat(frontends/lean/elaborator): improve error message
|
2016-09-03 13:21:54 -07:00 |
|
Leonardo de Moura
|
02316c39b8
|
feat(frontends/lean/elaborator): throw an error if a local instance is declared in the middle of a declaration
|
2016-09-01 18:06:38 -07:00 |
|
Leonardo de Moura
|
e061e9acab
|
refactor(frontends/lean/elaborator): remove elaborator::ctx()
The plan is to make `type_context` a transient object in the elaborator.
|
2016-09-01 08:28:30 -07:00 |
|
Leonardo de Moura
|
381f2dc434
|
chore(frontends/lean/elaborator): simplify mk_pp_ctx
|
2016-09-01 08:15:36 -07:00 |
|
Leonardo de Moura
|
001991dbeb
|
feat(frontends/lean): use equations_header
|
2016-08-30 13:45:59 -07:00 |
|
Leonardo de Moura
|
16a99436b4
|
fix(frontends/lean/elaborator): make sure all inductive datatype parameters in constructor applications are marked as inaccessible
|
2016-08-28 07:58:18 -07:00 |
|
Leonardo de Moura
|
b37b4f3dc8
|
fix(frontends/lean/elaborator): implicit terms are marked as inaccessible in patterns
|
2016-08-28 07:58:06 -07:00 |
|
Leonardo de Moura
|
ae63821cdb
|
fix(frontends/lean/elaborator): reject inaccessible annotation inside inaccessible annotation
|
2016-08-28 07:57:44 -07:00 |
|
Leonardo de Moura
|
7b37762231
|
fix(frontends/lean/elaborator): make sure elaborated term is based on what the user wrote
|
2016-08-28 07:57:34 -07:00 |
|
Leonardo de Moura
|
55bd3e223e
|
feat(library/type_context): add set_env
|
2016-08-23 18:32:58 -07:00 |
|
Leonardo de Moura
|
a93eada058
|
feat(library/type_context): improved (and simplified) cache management for type_context
|
2016-08-23 17:56:58 -07:00 |
|
Leonardo de Moura
|
7e4f15b0d8
|
feat(frontends/lean/elaborator): more inaccessible term validation
|
2016-08-19 14:52:11 -07:00 |
|
Leonardo de Moura
|
7a0158dcab
|
fix(frontends/lean/elaborator): must take (updated) configuration options into account
|
2016-08-18 15:47:49 -07:00 |
|
Leonardo de Moura
|
e6212469f0
|
feat(library/type_context): add helper functions for pretty printing
|
2016-08-18 15:36:01 -07:00 |
|
Leonardo de Moura
|
160632564d
|
fix(frontends/lean/elaborator): prevent unintended copy of type_context
|
2016-08-18 14:31:18 -07:00 |
|
Leonardo de Moura
|
ddc3789929
|
feat(frontends/lean): add run_tactic command
This commit also adds the tactic `add_decl`.
|
2016-08-18 10:56:18 -07:00 |
|
Leonardo de Moura
|
7059609f57
|
feat(library/equations_compiler): equations_compiler stub, add helper equations_editor, add preprocessing
The first preprocessing step packs nary functions into unary using sigma types
|
2016-08-14 17:02:36 -07:00 |
|
Leonardo de Moura
|
ed2a63ae89
|
feat(frontends/lean/elaborator): elaborate equations
|
2016-08-13 21:37:25 -07:00 |
|
Leonardo de Moura
|
150ad5d292
|
feat(frontends/lean/elaborator): elaborate convoy idiom
|
2016-08-13 20:51:42 -07:00 |
|
Leonardo de Moura
|
9e3bf4bd8d
|
fix(frontends/lean/elaborator): improve error message for eliminator elaborator
|
2016-08-13 15:43:44 -07:00 |
|
Leonardo de Moura
|
527ce72d2f
|
feat(frontends/lean/elaborator): add elaborate_with_type
|
2016-08-13 13:33:37 -07:00 |
|
Leonardo de Moura
|
f5c35f8d76
|
chore(*): fix compilation warnings
|
2016-08-10 18:03:13 -07:00 |
|
Leonardo de Moura
|
8f33269286
|
feat(frontends/lean): add decl_util module for definition/inductive commands
|
2016-08-10 17:04:12 -07:00 |
|
Leonardo de Moura
|
ae6219ba28
|
refactor(frontends/lean/elaborator): improve API
|
2016-08-10 14:34:54 -07:00 |
|
Leonardo de Moura
|
8498bbaeff
|
refactor(frontends/lean/elaborator): allow elaborator to add auxiliary definitions
|
2016-08-10 08:31:00 -07:00 |
|
Leonardo de Moura
|
e5cf12e2ad
|
refactor(frontends/lean/elaborator): cleanup interface
|
2016-08-10 08:20:10 -07:00 |
|
Leonardo de Moura
|
1041f6d9d8
|
feat(frontends/lean/structure_cmd): private structures
|
2016-08-06 00:03:06 -07:00 |
|
Leonardo de Moura
|
276b47688f
|
feat(frontends/lean/elaborator): uvar => param at top-level
|
2016-08-05 18:24:37 -07:00 |
|
Leonardo de Moura
|
befe2d96e1
|
feat(frontends/lean/elaborator): chaining for anonymous constructors
|
2016-08-04 15:08:25 -07:00 |
|
Leonardo de Moura
|
8b05fba6ef
|
feat(frontends/lean/elaborator): propagate expected type to arguments when elaborating constructors
|
2016-08-04 14:07:15 -07:00 |
|
Leonardo de Moura
|
6a0d9dab40
|
feat(frontends/lean/elaborator): anonymous constructors
|
2016-08-04 13:03:49 -07:00 |
|
Leonardo de Moura
|
794382da01
|
feat(frontends/lean/elaborator): take care of foreign universe metavars in the sanitizer
|
2016-08-03 14:13:42 -07:00 |
|
Leonardo de Moura
|
e87b54988b
|
feat(frontends/lean/elaborator): minor cleanup
|
2016-08-03 13:25:49 -07:00 |
|
Leonardo de Moura
|
2c8e484aa3
|
feat(frontends/lean/elaborator): universe parameter name sanitizer
|
2016-08-03 13:13:44 -07:00 |
|
Leonardo de Moura
|
112aae2928
|
feat(frontends/lean/elaborator): erase info annotations
|
2016-08-02 15:43:23 -07:00 |
|
Leonardo de Moura
|
ee46befd26
|
chore(frontends/lean/elaborator): cleanup
|
2016-08-02 13:16:43 -07:00 |
|
Leonardo de Moura
|
babc8906b3
|
fix(library/metavar_util): but in instantiate_mvars
|
2016-08-02 13:16:17 -07:00 |
|
Leonardo de Moura
|
c91a7a8e9b
|
fix(frontends/lean/elaborator): add checkpoint
|
2016-08-02 10:10:11 -07:00 |
|
Leonardo de Moura
|
139707413c
|
fix(frontends/lean/elaborator): better position information
|
2016-08-02 10:00:05 -07:00 |
|
Leonardo de Moura
|
90f5dabf28
|
fix(frontends/lean/elaborator): order type class instances are synthesized
|
2016-08-01 23:59:22 -07:00 |
|
Leonardo de Moura
|
dd98c86a79
|
fix(frontends/lean/elaborator): as_atomic elaboration
|
2016-08-01 23:26:34 -07:00 |
|