Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Leonardo de Moura
e358a15dd4
fix(frontends/lean/elaborator): show-goal-at-pos after last tactic
...
See issue #1169
2016-10-25 02:40:24 +08:00
Gabriel Ebner
5f803c0353
feat(frontends/lean/elaborator): make show-goal-at-pos work on
...
by-tactics
2016-10-21 15:42:29 -07:00
Gabriel Ebner
47e6fd091f
refactor(frontends/lean): implement show goal function using exceptions
2016-10-21 15:42:29 -07:00
Leonardo de Moura
1185799b1f
feat(frontends/lean/elaborator): more detailed error message for a^.f notation
2016-10-18 16:22:05 -07:00
Leonardo de Moura
9b84db083d
fix(frontends/lean): error localization bugs
2016-10-15 13:40:57 -07:00
Leonardo de Moura
c3861c7ab3
fix(frontends/lean/elaborator): bug when creating error message
2016-10-15 13:30:26 -07:00
Leonardo de Moura
a5029ab5d2
fix(frontends/lean): improve error localization
2016-10-15 10:43:33 -07:00
Gabriel Ebner
66be9c31db
refactor(library/flycheck): use flycheck_message_stream instead of option
2016-10-13 18:49:10 -07:00
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
