Gabriel Ebner
5acb722d46
refactor(library/flycheck,library/trace): convert trace output to messages independently of flycheck
2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2
refactor(*): structured message objects
2016-10-13 18:49:10 -07:00
Gabriel Ebner
37b998ff1e
feat(frontends/lean,library/flycheck): redirect all diagnostic output from commands to flycheck
2016-10-08 22:23:53 -07:00
Gabriel Ebner
996b4375a9
feat(library/flycheck,frontends/lean/elaborator): show trace messages in flycheck
2016-10-05 15:20:00 -07:00
Leonardo de Moura
d252f4ac7d
feat(frontends/lean/elaborator): improve mini-lenses
2016-10-03 20:17:45 -07:00
Leonardo de Moura
16985d0de1
feat(frontends/lean/elaborator): better error message for eval_expr
2016-10-03 18:23:47 -07:00
Leonardo de Moura
7465529445
feat(library/tactic): 'eval_expr' tactic skeleton
2016-10-03 16:26:28 -07:00
Leonardo de Moura
1baa953b48
feat(frontends/lean/elaborator): improve error localization
2016-10-02 13:33:49 -07:00
Leonardo de Moura
838b3329ce
fix(frontends/lean/elaborator): structure instance update with type classes
2016-10-02 11:36:22 -07:00
Leonardo de Moura
5726d45e7f
fix(frontends/lean/elaborator): bad error msg
2016-09-29 15:23:20 -07:00
Leonardo de Moura
f97e238b8e
feat(frontends/lean/elaborator): decorate error messages when overloads are used
2016-09-29 15:00:45 -07:00
Leonardo de Moura
f2e8b8794c
feat(frontends/lean/elaborator): display error when failed to elaborate using expected type
2016-09-29 11:55:05 -07: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
c8a720212b
feat(frontends/lean): 'by' is now also using interactive mode syntax
2016-09-29 01:57:40 -07:00
Leonardo de Moura
84b45b010a
feat(frontends/lean/elaborator): improve overloading support
2016-09-28 20:54:11 -07:00
Leonardo de Moura
1f07e87bc2
refactor(frontends/lean/elaborator): add first_pass_info struct
2016-09-28 20:54:10 -07:00
Leonardo de Moura
6e6609f2aa
fix(frontends/lean): use coercions to sort at elaborate_type
2016-09-26 16:47:31 -07:00
Leonardo de Moura
dd8018eb04
fix(frontends/lean/elaborator): make coercion resolution more robust
2016-09-26 16:18:36 -07:00
Leonardo de Moura
b9b64b121c
feat(frontends/lean/elaborator): add show-goal support (Ctrl-c-g on Emacs)
2016-09-26 11:19:08 -07:00
Leonardo de Moura
78c6bc3a26
feat(frontends/lean): add step-by-step 'begin...end' block execution
2016-09-26 10:56:40 -07:00
Leonardo de Moura
3c71d7eda2
feat(frontends/lean,library/tactic/tactic_state): improve error localization
2016-09-25 18:40:41 -07:00
Leonardo de Moura
264b614f0d
fix(frontends/lean/elaborator): bug when checking for unassigned metavars
2016-09-25 17:22:45 -07:00
Leonardo de Moura
177840bc36
fix(frontends/lean/elaborator): structure instance notation {...} for structures that have implicit fields
2016-09-23 11:32:12 -07:00
Leonardo de Moura
f9eaab8130
feat(frontends/lean/definition_cmds): improve error minimization
2016-09-23 10:16:46 -07:00
Leonardo de Moura
9a1ef1cc0d
fix(frontends/lean/elaborator): 'sorry' in quoted expressions
2016-09-23 09:34:00 -07:00
Leonardo de Moura
c8e13cd391
feat(frontends/lean): minimize errors being reported
2016-09-23 09:20:31 -07:00
Leonardo de Moura
7ae778e925
feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>'
2016-09-23 08:18:19 -07:00
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
