Leonardo de Moura
c3ce9d0a2d
fix(frontends/lean): bug that only happens in newer versions of g++
...
See #1098
I only managed to reproduce the bug after I installed Ubuntu 16.04
2016-08-01 21:57:11 -07:00
Leonardo de Moura
a1854df9fa
test(tests/lean/run/elab_crash1): add new test
2016-08-01 17:26:47 -07:00
Leonardo de Moura
582117da96
fix(frontends/lean/elaborator): elaborator must take into account binder information when caching inferred types
2016-08-01 16:35:42 -07:00
Leonardo de Moura
a50e13f538
feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information
2016-08-01 16:34:07 -07:00
Leonardo de Moura
8127ba9a5f
feat(frontends/lean/parser): adapter for converting local_expr_decls ==> local_context
2016-08-01 14:52:01 -07:00
Leonardo de Moura
d46e9b411c
fix(frontends/lean/elaborator): spurious universe parameters being generated
2016-08-01 08:10:15 -07:00
Leonardo de Moura
5b33c0384d
test(tests/lean/run/qexpr1): add test for nested quotes
2016-08-01 07:42:06 -07:00
Leonardo de Moura
c1793cd620
feat(library/init/meta/tactic): add 'refine' tactic
2016-07-31 21:17:19 -07:00
Leonardo de Moura
fefa5ad3b8
fix(library/tactic/elaborate): new subgoals must be inserted after main goal
2016-07-31 21:16:29 -07:00
Leonardo de Moura
bf0d7b3ff2
fix(library/quote): add quote macro reader
2016-07-31 21:15:03 -07:00
Leonardo de Moura
fb49d61042
chore(frontends/lean): fix warnings and remove dead code
2016-07-31 20:53:26 -07:00
Leonardo de Moura
7ddc3c72dd
fix(frontends/lean/elaborator, library/vm/vm_qexpr): add and handle as_is annotation
2016-07-31 20:49:53 -07:00
Leonardo de Moura
6d0fa806d8
feat(library/tactic/elaborate): convert unassigned metavars into new goals
2016-07-31 20:38:57 -07:00
Leonardo de Moura
12fa52c77d
feat(library/tactic, frontends/lean/elaborator): add to_expr tactic
2016-07-31 20:21:17 -07:00
Leonardo de Moura
09c000fcb8
chore(frontends/lean/elaborator): remove unnecessary field
2016-07-31 19:54:04 -07:00
Leonardo de Moura
68ad696777
chore(frontends/lean/nested_declaration): do not allow attributes in abstract ... end blocks
2016-07-31 19:14:33 -07:00
Leonardo de Moura
da98191256
chore(tests/lean/run): preparing tests for new elaborator
2016-07-31 17:45:43 -07:00
Leonardo de Moura
42958be45f
feat(frontends/lean/elaborator): better get_level
2016-07-31 17:45:02 -07:00
Leonardo de Moura
e5298c9d8f
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
...
The new encoding is better for the new elaborator.
2016-07-31 17:14:01 -07:00
Leonardo de Moura
9fc222b9af
chore(library/pp_options): remove option pp.metavar_args
2016-07-31 16:00:21 -07:00
Leonardo de Moura
c983e46daa
fix(frontends/lean/elaborator): make sure error messages are not affected by purify_metavars
2016-07-31 15:53:30 -07:00
Leonardo de Moura
138d1bb146
fix(library/type_context): missing case
2016-07-31 15:16:52 -07:00
Leonardo de Moura
215bd214ef
chore(frontends/lean/elaborator): add another trace msg
2016-07-31 15:10:36 -07:00
Leonardo de Moura
877bfe0250
fix(frontends/lean/pp): pp_meta bug
2016-07-31 14:54:37 -07:00
Leonardo de Moura
f461b53a7f
refactor(library): remove eq.ops namespace
2016-07-31 12:50:11 -07:00
Leonardo de Moura
1aeda0e74b
feat(frontends/lean/elaborator): invoke tactics
2016-07-31 11:56:52 -07:00
Leonardo de Moura
e28e4fc896
feat(frontends/lean/elaborator): convert unassigned universe levels into universe parameters, basic support for by tactic
2016-07-31 03:45:18 -07:00
Leonardo de Moura
c46403265b
feat(library/local_context): add instance_mvars method for local_context object
2016-07-31 02:36:51 -07:00
Leonardo de Moura
f72f9dd561
fix(frontends/lean/pp): purify metavar_decl_ref's
...
The tests become too fragile if we don't purify them.
2016-07-30 20:30:03 -07:00
Leonardo de Moura
96ec2e5914
fix(library/type_context): missing case
2016-07-30 20:04:56 -07:00
Leonardo de Moura
1b528ba327
chore(util/name): remove assertion
...
The procedure get_tagged_name_suffix violates the assertion.
Alternative solution: change return type of get_tagged_name_suffix to
optional<std::string> since it is only used for pretty printing.
2016-07-30 19:53:58 -07:00
Leonardo de Moura
fafea473b8
feat(frontends/lean/elaborator): coercions to sort
2016-07-30 19:47:04 -07:00
Leonardo de Moura
5c6ee38181
fix(library/type_context): reject instances containing tmp universe metavars
2016-07-30 19:43:34 -07:00
Leonardo de Moura
b4fefd8c0b
feat(frontends/lean/elaborator): coercions to functions
2016-07-30 18:54:20 -07:00
Leonardo de Moura
b6139ab59d
fix(library/type_context): bug in type class resolution
2016-07-30 15:54:28 -07:00
Leonardo de Moura
8b533a54c2
feat(frontends/lean/pp): improve purify_metavars
2016-07-30 15:31:06 -07:00
Leonardo de Moura
44a77f6907
test(tests/lean/coe1): add coercion tests
2016-07-30 12:29:12 -07:00
Leonardo de Moura
f18c84ca59
feat(frontends/lean/pp): add option for hiding coercions
2016-07-30 12:25:18 -07:00
Leonardo de Moura
68f73851d9
test(tests/lean/elab4b): test error messages when pp.full_names is false
2016-07-30 12:02:14 -07:00
Leonardo de Moura
a0589ce8b8
feat(frontends/lean): automatic coercions
2016-07-30 11:53:25 -07:00
Leonardo de Moura
32eb37472f
feat(library/init/coe): make sure base case is tried before transitive case, add (decidable (coe b)) instance
2016-07-30 11:44:05 -07:00
Leonardo de Moura
4f72fa5fc5
feat(library/type_context): add trace.type_context.univ_is_def_eq and trace.type_context.univ_is_def_eq_detail
2016-07-30 11:14:36 -07:00
Leonardo de Moura
2ad5c2ab73
feat(library/init): add has_lift has_coe has_coe_to_fun type classes
2016-07-30 10:11:30 -07:00
Leonardo de Moura
671784e35f
chore(tests/lean/pp_all2): fix test output
2016-07-29 23:35:10 -07:00
Leonardo de Moura
29f79d71e3
chore(library): remove dead code
2016-07-29 23:32:36 -07:00
Leonardo de Moura
0169989411
chore(library/class): remove transitive instance support
...
Conflicts:
src/frontends/lean/structure_cmd.cpp
src/library/class.cpp
src/library/class.h
2016-07-29 23:32:10 -07:00
Leonardo de Moura
4a0eb15a5c
chore(library/type_context): remove support for transitive instances
2016-07-29 23:28:51 -07:00
Leonardo de Moura
264c23a24f
chore(library/class): disable [trans_instance] attribute
...
Conflicts:
src/library/class.cpp
2016-07-29 23:28:36 -07:00
Sebastian Ullrich
03b1daa0bf
feat(bin): GDB pretty printer for lean::buffer
2016-07-29 23:44:29 -04:00
Sebastian Ullrich
e090326f98
fix(library): remove classical instances from global scope
2016-07-29 23:44:23 -04:00
