Leonardo de Moura
|
52b66a1573
|
chore(frontends/lean/pp, library/pp_options): pp.lazy_abstraction ==> pp.delayed_abstraction
|
2016-08-03 18:45:47 -07:00 |
|
Daniel Selsam
|
70a1e53ba8
|
feat(simplifier/simp_lemmas): take arbitrary list of attributes and cache
|
2016-08-03 18:04:28 -07:00 |
|
Leonardo de Moura
|
1ca15e9b42
|
chore(frontends/lean): remove obtain-expr dead code
|
2016-08-03 17:41:16 -07:00 |
|
Leonardo de Moura
|
594c7ca4c5
|
chore(frontends/lean/find_cmd): remove find_decl command
|
2016-08-03 17:32:47 -07:00 |
|
Leonardo de Moura
|
971a5dae69
|
refactor(frontends/lean/inductive_cmd): replace old_type_checker_ptr with type_context
|
2016-08-03 17:29:09 -07:00 |
|
Leonardo de Moura
|
f4e1e92807
|
feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands
|
2016-08-03 17:10:45 -07:00 |
|
Leonardo de Moura
|
b6be493cef
|
feat(frontends/lean/util): elaborate priority/precedence expressions using the new elaborator
|
2016-08-03 17:01:34 -07:00 |
|
Leonardo de Moura
|
aeafe0293b
|
feat(frontends/lean/structure_cmd): use new elaborator to process the structure command
|
2016-08-03 16:56:41 -07:00 |
|
Leonardo de Moura
|
d473622352
|
refactor(frontends/lean/structure_cmd): remove unnecessary options
|
2016-08-03 15:48:58 -07:00 |
|
Leonardo de Moura
|
794382da01
|
feat(frontends/lean/elaborator): take care of foreign universe metavars in the sanitizer
|
2016-08-03 14:13:42 -07:00 |
|
Leonardo de Moura
|
e87b54988b
|
feat(frontends/lean/elaborator): minor cleanup
|
2016-08-03 13:25:49 -07:00 |
|
Leonardo de Moura
|
2c8e484aa3
|
feat(frontends/lean/elaborator): universe parameter name sanitizer
|
2016-08-03 13:13:44 -07:00 |
|
Leonardo de Moura
|
4e80094927
|
feat(frontends/lean/inductive_cmd): use new elaborator in the inductive command
|
2016-08-03 13:13:12 -07:00 |
|
Leonardo de Moura
|
112aae2928
|
feat(frontends/lean/elaborator): erase info annotations
|
2016-08-02 15:43:23 -07:00 |
|
Leonardo de Moura
|
186d82d58d
|
chore(frontends/lean/builtin_cmds): remove dead code
|
2016-08-02 15:18:05 -07:00 |
|
Leonardo de Moura
|
8993d0738a
|
feat(frontends/lean): remove #elab command
The check command is now using the new elaborator.
|
2016-08-02 15:05:24 -07:00 |
|
Leonardo de Moura
|
dc44edfd41
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
Leonardo de Moura
|
dcba76ba7e
|
feat(frontends/lean/parser): at parser::elaborate convert metavar_decl_ref's into regular metavars
|
2016-08-02 14:45:04 -07:00 |
|
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
|
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
|
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
|
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
|
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
|
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
|
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
|
fafea473b8
|
feat(frontends/lean/elaborator): coercions to sort
|
2016-07-30 19:47:04 -07:00 |
|
Leonardo de Moura
|
b4fefd8c0b
|
feat(frontends/lean/elaborator): coercions to functions
|
2016-07-30 18:54:20 -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
|
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 |
|