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
|
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
|
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
|
8127ba9a5f
|
feat(frontends/lean/parser): adapter for converting local_expr_decls ==> local_context
|
2016-08-01 14:52:01 -07:00 |
|
Leonardo de Moura
|
09c000fcb8
|
chore(frontends/lean/elaborator): remove unnecessary field
|
2016-07-31 19:54:04 -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
|
1aeda0e74b
|
feat(frontends/lean/elaborator): invoke tactics
|
2016-07-31 11:56:52 -07:00 |
|
Sebastian Ullrich
|
e69b508492
|
refactor(library/export_decl): Re-implement for new scoped_ext
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
|
2016-07-29 23:44:22 -04:00 |
|
Leonardo de Moura
|
931251d403
|
feat(frontends/lean): remove local_context from parser
|
2016-07-28 16:19:31 -07:00 |
|
Leonardo de Moura
|
dcf0244ecd
|
chore(frontends/lean/parser): remove dead code
|
2016-07-28 09:56:03 -07:00 |
|
Leonardo de Moura
|
e6627cdfc1
|
feat(frontends/lean/parser): add new_elaborator option
|
2016-07-28 09:48:12 -07:00 |
|
Leonardo de Moura
|
3a5f6f2e64
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
Leonardo de Moura
|
3218f91e35
|
feat(frontends/lean): add support for character literals
|
2016-07-18 14:07:10 -04:00 |
|
Leonardo de Moura
|
f34e84dacb
|
feat(frontends/lean/parser): cute binders
|
2016-07-08 07:50:58 -07:00 |
|
Leonardo de Moura
|
58569b82d3
|
refactor(frontends/lean,library,library/tactic): move type_context_cache_helper to type_context module
|
2016-06-30 12:03:40 +01:00 |
|
Leonardo de Moura
|
1a5756661f
|
refactor(frontends/lean,library): move scope_pos_info_provider to library
|
2016-06-30 10:19:35 +01:00 |
|
Leonardo de Moura
|
bb70fbbd48
|
refactor(frontends/lean): simplify elaborator_context
|
2016-06-29 16:56:19 +01:00 |
|
Leonardo de Moura
|
ccc65c6171
|
refactor(frontends/lean): add thread local parser_pos_provider
|
2016-06-29 16:09:06 +01:00 |
|
Leonardo de Moura
|
f3803c6ee4
|
refactor(frontends/lean/elaborator_context): remove io_state from elaborator_context
|
2016-06-27 06:29:54 +01:00 |
|
Leonardo de Moura
|
2ea8b26c4f
|
refactor(library/io_state): move get_global_ios to io_state module
|
2016-06-25 20:59:52 -07:00 |
|
Leonardo de Moura
|
77286e6abb
|
fix(frontends/lean): replay exported decls in imported files
|
2016-06-25 12:13:36 -07:00 |
|
Leonardo de Moura
|
586baa4118
|
feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend
TODO: invoke elaborator at tactic.to_expr
|
2016-06-15 16:06:39 -07:00 |
|
Leonardo de Moura
|
3996f9db4d
|
feat(frontends/lean): add ( token and remove token
|
2016-06-15 13:22:31 -07:00 |
|
Leonardo de Moura
|
5459e9ad8a
|
chore(frontends/lean): remove dead code
|
2016-06-13 10:42:38 -07:00 |
|
Leonardo de Moura
|
b54203f6b3
|
feat(frontends/lean): parse by-expression
|
2016-06-13 10:25:26 -07:00 |
|
Leonardo de Moura
|
d302514933
|
chore(frontends/lean): remove tactic notation
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
e7b47a504e
|
feat(frontends/lean): add meta_definition and meta_constant commands
|
2016-06-01 09:12:41 -07:00 |
|
Leonardo de Moura
|
6a9e5079c9
|
feat(library,frontends/lean/pp): add support for new string encoding
|
2016-05-24 16:20:43 -07:00 |
|
Leonardo de Moura
|
fdea718d9d
|
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
|
2016-04-25 15:41:12 -07:00 |
|
Leonardo de Moura
|
d88098f38d
|
chore(frontends/lean): remove some of the tactic support
|
2016-04-25 15:26:56 -07:00 |
|
Leonardo de Moura
|
d66406a1f4
|
feat(frontends/lean): add #elab command for testing new elaborator
|
2016-04-05 17:03:23 -07:00 |
|
Leonardo de Moura
|
03809e7973
|
refactor(frontends/lean): elaborator_context
|
2016-04-05 16:19:06 -07:00 |
|
Leonardo de Moura
|
a1bc662eca
|
dev(frontends/lean/parser): add local_context
|
2016-03-30 16:33:17 -07:00 |
|
Leonardo de Moura
|
06ef0ad7be
|
refactor(frontends/lean): add local_level_decls
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
|
2016-03-30 15:47:32 -07:00 |
|
Leonardo de Moura
|
c4f25cf15b
|
refactor(frontends/lean): rename elaborate methods
|
2016-03-30 15:05:24 -07:00 |
|
Leonardo de Moura
|
75549bafd7
|
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
|
2016-03-30 14:59:18 -07:00 |
|
Leonardo de Moura
|
eaac6ba721
|
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
|
2016-03-04 10:26:50 -08:00 |
|
Leonardo de Moura
|
3c878ecd01
|
feat(kernel): add let-expressions to the kernel
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
|
2016-02-29 16:40:17 -08:00 |
|
Leonardo de Moura
|
f54963bc3e
|
refactor(library/tactic/expr_to_tactic): remove 'by_plus' support
|
2016-02-29 13:50:05 -08:00 |
|
Leonardo de Moura
|
7d61f640f6
|
refactor(*): add abstract_type_context class
|
2016-02-26 14:17:34 -08:00 |
|
Leonardo de Moura
|
c9e9fee76a
|
refactor(*): remove name_generator and use simpler mk_fresh_name
|
2016-02-11 18:05:57 -08:00 |
|
Leonardo de Moura
|
9cbda49297
|
chore(frontends/lean): remove script blocks
|
2016-02-11 17:26:44 -08:00 |
|
Leonardo de Moura
|
f67181baf3
|
chore(*): remove support for Lua
|
2016-02-11 17:17:55 -08:00 |
|
Leonardo de Moura
|
b92416d66c
|
refactor(library/error_handling): move error_handling to library main dir
|
2015-12-29 15:31:40 -08:00 |
|
Leonardo de Moura
|
cac10aa728
|
fix(frontends/lean/parser): allow '...' token to be used in imports
Before this commit, we could not write
import ...foo.b
We had to write
import .. .foo.b
or
import . ..foo.b
|
2015-12-28 09:08:18 -08:00 |
|
Leonardo de Moura
|
61ecf018e9
|
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
|
2015-12-17 12:18:32 -08:00 |
|
Leonardo de Moura
|
2502039a5c
|
fix(frontends/lean/parser): tactic notation that may take numerical parameters
|
2015-12-17 11:27:31 -08:00 |
|
Leonardo de Moura
|
727a4f5a3a
|
feat(library/tactic/intros_tactic): use '_' to say that some names are irrelevant in the intro tactic
See #695
|
2015-12-13 16:47:31 -08:00 |
|