Leonardo de Moura
b55a17614a
feat(frontends/lean): structure instances
2016-09-21 22:52:43 -07:00
Leonardo de Moura
b67216374c
feat(frontends/lean): projection notation
2016-09-21 11:14:41 -07:00
Leonardo de Moura
335242e9f1
chore(frontends/lean): remove info_annotation module
2016-09-19 21:19:31 -07:00
Leonardo de Moura
10f4a22fff
fix(frontends/lean/elaborator): try to synthesize pending type class instances before processing eliminator/recursor
2016-09-19 11:14:49 -07:00
Leonardo de Moura
677d3d4cf9
fix(frontends/lean/elaborator): ignore annotations around function when deciding which kind of elaborator strategy should be used
2016-09-18 19:10:13 -07:00
Leonardo de Moura
4c15c9833d
fix(frontends/lean/elaborator): use_elim_elab_core
2016-09-17 20:04:14 -07:00
Leonardo de Moura
90bfd84a07
feat(frontends/lean): Type is now (Type 1)
...
In the standard library, we should use explicit universe variables for
universe polymorphic definitions.
Users that want to declare universe polymorphic definitions but do not
want to provide universe level parameters should use
Type _
or
Type*
2016-09-17 14:30:54 -07:00
Leonardo de Moura
9c8b7be225
chore(frontends/lean/elaborator): improve error message
2016-09-15 18:47:32 -07:00
Leonardo de Moura
80ddb0e706
feat(frontends/lean/elaborator): use type class resolution for _ arguments even when @ (or @@) is used
2016-09-15 17:29:38 -07:00
Leonardo de Moura
25714d71a2
refactor(frontends/lean/elaborator): rename visit_default_app since it is not the "default" elaboration strategy anymore
2016-09-15 17:14:01 -07:00
Leonardo de Moura
f60de96d98
fix(frontends/lean/elaborator): bug at @@ annotation
2016-09-15 17:03:59 -07:00
Leonardo de Moura
f42afe2b65
feat(frontends/lean/elaborator): [elab_with_expected_type] is the new default strategy
2016-09-15 14:45:52 -07:00
Leonardo de Moura
5d3765a6b7
fix(frontends/lean/elaborator): missing instantiate_mvars
2016-09-15 13:59:09 -07:00
Leonardo de Moura
6a331e2ab8
feat(frontends/lean/elaborator): better error message when there is a mismatch between inferred and synthesized instances
2016-09-15 09:05:19 -07:00
Leonardo de Moura
8d51607ea0
chore(frontends/lean/elaborator): remove verbose trace message
2016-09-14 18:14:53 -07:00
Leonardo de Moura
59ce650033
feat(frontends/lean/elaborator): improve how type class instances are handled at visit_app_with_expected
2016-09-14 18:07:01 -07:00
Leonardo de Moura
0ff5733d70
refactor(frontends/lean/elaborator): checkpoints
2016-09-14 17:29:51 -07:00
Leonardo de Moura
b426119e83
chore(frontends/lean/elaborator): rename attribute [elab_default] ==> [elab_simple]
2016-09-14 09:42:30 -07:00
Leonardo de Moura
9bb8b0e6ef
feat(frontends/lean/elaborator): always use approximate is_def_eq in the elaborator
2016-09-14 09:01:09 -07:00
Leonardo de Moura
9461595a70
chore(frontends/lean/elaborator): remove leftover
2016-09-13 21:55:55 -07:00
Leonardo de Moura
2ff3e4aaeb
feat(frontends/lean/elaborator): better error position
2016-09-13 16:17:50 -07:00
Leonardo de Moura
cf1c50f4e9
fix(frontends/lean/elaborator): get_elim_info_for_builtin
2016-09-13 14:17:08 -07:00
Leonardo de Moura
5f8f7bcccb
feat(frontends/lean/elaborator): add proxy_attribute for elaborator strategies
...
This commit also adds a template for creating proxy_attribute's.
2016-09-13 13:02:37 -07:00
Leonardo de Moura
0d166970de
fix(frontends/lean/elaborator): missing instantiate_mvars
2016-09-13 08:09:12 -07:00
Leonardo de Moura
d79fbee421
fix(frontends/lean/elaborator): visit_app_with_expected
...
Mark ite and dite with elab_with_expected_type.
2016-09-12 16:48:21 -07:00
Leonardo de Moura
aa2f9fadee
feat(frontends/lean/elaborator): add support for nondependent eliminators in the new elaborator
2016-09-12 15:26:13 -07:00
Leonardo de Moura
24f76d5260
feat(frontends/lean/elaborator): improve convoy and elim
2016-09-10 22:51:26 -07:00
Leonardo de Moura
61f7702940
feat(frontends/lean/elaborator): disable checks
2016-09-10 22:50:29 -07:00
Leonardo de Moura
f53ff9a3b6
feat(frontends/lean/elaborator): add [elab_as_eliminator] attribute
2016-09-10 21:58:30 -07:00
Leonardo de Moura
214e91d1ae
feat(frontends/lean/elaborator): improve match_convoy in the new elaborator
2016-09-10 21:41:40 -07:00
Leonardo de Moura
4d06f71e72
chore(frontends/lean/elaborator): remove unnecessary procedure
2016-09-10 21:14:58 -07:00
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
