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
860d333b5e
fix(src/library/type_context): unifier first-order approximation
2016-08-02 09:51:18 -07:00
Leonardo de Moura
53da866935
feat(library/init/meta/simp_tactic): add tactic for creating empty simp_lemmas
2016-08-02 09:00:49 -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
Leonardo de Moura
5ffbc2f94e
fix(library/vm/vm): memory leak
2016-08-01 23:06:53 -07:00
Leonardo de Moura
219300e923
fix(frontends/lean/elaborator): erase 'as_atomic' annotation
2016-08-01 23:06:41 -07:00
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
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
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
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
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
f18c84ca59
feat(frontends/lean/pp): add option for hiding coercions
2016-07-30 12:25:18 -07:00
Leonardo de Moura
a0589ce8b8
feat(frontends/lean): automatic coercions
2016-07-30 11:53:25 -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
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
5247b426a8
fix(library/reducible): use class hierarchy to fix reducibility attributes
2016-07-29 23:44:22 -04:00
Sebastian Ullrich
31f599e088
refactor(library/attribute_manager): introduce hierarchy of attribute classes
2016-07-29 23:44:22 -04:00
