Sebastian Ullrich
a2659cdaa5
feat(frontends/lean/decl_attributes): add [attr1, attr2] syntax
2016-08-16 13:49:03 -07:00
Sebastian Ullrich
e15e085126
refactor(frontends/lean/old_attributes, library/tactic/backward/backward_lemmas): merge [intro] and [intro!] attributes
2016-08-16 13:49:03 -07:00
Leonardo de Moura
f5c35f8d76
chore(*): fix compilation warnings
2016-08-10 18:03:13 -07:00
Leonardo de Moura
a0a72b5b82
refactor(frontends/lean): move local_context_adapter to separate folder
2016-08-10 07:52:38 -07:00
Leonardo de Moura
1602a53336
feat(frontends/lean): nary match
2016-08-08 10:04:58 -07:00
Leonardo de Moura
1e6b3614ab
feat(frontends/lean): new pattern matching validation
...
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
2016-08-07 11:31:11 -07:00
Leonardo de Moura
d36280f74f
refactor(frontends/lean): id_behavior
2016-08-07 08:07:24 -07:00
Leonardo de Moura
fb8ae7f411
chore(frontends/lean/parser): add comment
2016-08-06 13:24:10 -07:00
Sebastian Ullrich
15595c0061
refactor(library/attribute_manager): delegate parameter parsing and printing to attribute class
2016-08-05 17:16:04 -07:00
Leonardo de Moura
b6420904f5
feat(frontends/lean): resolved quoted names
2016-08-05 17:04:36 -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
e87b54988b
feat(frontends/lean/elaborator): minor cleanup
2016-08-03 13:25:49 -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
1aeda0e74b
feat(frontends/lean/elaborator): invoke tactics
2016-07-31 11:56:52 -07: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
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
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
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
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
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -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
20de22a8ad
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included)
2015-12-13 13:20:54 -08:00
Leonardo de Moura
a9b567296c
feat(frontends/lean/parser): add anonymous inst implicit name generator
2015-12-13 11:46:48 -08:00
Leonardo de Moura
d26a83da02
feat(frontends/lean/parser): allow anonymous instance implicit arguments
2015-12-13 11:46:48 -08:00
Leonardo de Moura
cf61adc5d5
feat(frontends/lean): identifiers starting with '_' are now reserved
2015-12-10 22:32:03 -08:00
Leonardo de Moura
1abaa9eb71
fix(frontends/lean/parser): fixes #858
2015-12-10 10:31:14 -08:00
Leonardo de Moura
3f9549485f
feat(frontends/lean/parser): restore config options in the end of sections/namespaces
2015-12-09 11:24:37 -08:00
Leonardo de Moura
f84c6a6cfa
fix(library/blast,frontends/lean): handling pattern hints after unfolding
2015-12-02 22:52:55 -08:00
Leonardo de Moura
f78e57fd52
feat(shell,frontends/lean): add command line option --dir
...
See #821
See #788
2015-11-19 08:34:23 -08:00
Leonardo de Moura
d1e111fd6c
fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library
2015-11-08 14:04:55 -08:00
