Leonardo de Moura
a74f02546b
refactor(*): remove abbreviation command
2016-09-03 17:11:29 -07:00
Leonardo de Moura
803c956d18
feat(util/sexpr/option_declarations): allow options to be registered after initialization
2016-08-19 16:58:30 -07:00
Leonardo de Moura
ddc3789929
feat(frontends/lean): add run_tactic command
...
This commit also adds the tactic `add_decl`.
2016-08-18 10:56:18 -07:00
Sebastian Ullrich
cb6a6b642e
refactor(library/attribute_manager): remove attribute tokens and use name for attribute names
2016-08-16 13:49:03 -07:00
Leonardo de Moura
8f33269286
feat(frontends/lean): add decl_util module for definition/inductive commands
2016-08-10 17:04:12 -07:00
Leonardo de Moura
371dd9d1e1
refactor(frontends/lean): move match-expr parser to different module
2016-08-08 09:05:22 -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
dc44edfd41
feat(frontends/lean): use new elaborator in the 'check' command
2016-08-02 14:57:49 -07:00
Sebastian Ullrich
c4edad0372
feat(frontends/lean, library): remove attribute and metaclass scoping
...
All data is now part of either a global, permanent scope or a local,
temporary one
2016-07-29 23:44:21 -04:00
Leonardo de Moura
8333500457
refactor(library): move try_eta to util
2016-06-17 10:29:02 -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
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
56d7fc4c23
refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled
2016-02-29 16:55:19 -08:00
Leonardo de Moura
20f70035dd
fix(frontends/lean/util): fixes #1007
2016-02-22 10:54:55 -08:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Leonardo de Moura
45dbf76df9
refactor(library): add attribute manager
2015-12-17 20:58:15 -08:00
Leonardo de Moura
ce622e9179
feat(frontends/lean): add auto-include for structures and inductive decls
2015-12-13 13:39:34 -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
769da9c95a
fix(library/unifier): missing occurs check
2015-12-04 09:14:55 -08:00
Leonardo de Moura
38c433dbec
fix(frontends/lean/util): bug when parsing priorities
2015-11-08 14:04:55 -08:00
Leonardo de Moura
8ee214f133
checkpoint: new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
c84e886c7b
fix(frontends/lean/notation_cmd): fixes #808
...
This commit and 2b1d2c fixes #808
2015-08-31 18:05:58 -10:00
Leonardo de Moura
2b1d2c21ad
fix(frontends/lean/util): bug when parsing priorities and numerals are overloaded
2015-08-31 15:08:21 -10:00
Leonardo de Moura
66a59d5b51
feat(frontends/lean/util): remove hack that overrides priority namespace
...
closes #789
2015-08-11 18:01:40 -07:00
Leonardo de Moura
267545ca0c
feat(frontends/lean): parse 'with_options' tactical
...
see issue #492
2015-07-13 19:13:41 -04:00
Leonardo de Moura
a1d1a8272a
refactor(frontends/lean): move parse_priority to util
2015-06-30 16:22:52 -07:00
Leonardo de Moura
8b7dc4e03a
feat(frontends/lean): apply eta-reduction in postprocessing step
...
Perhaps, we should add an option to disable this new feature.
Remark: this commit makes commit 46d418a46d418a
2015-06-10 16:29:30 -07:00
Leonardo de Moura
ca43f6e62e
refactor(frontends/lean): add postprocess procedure and cleanup
2015-06-10 15:19:35 -07:00
Leonardo de Moura
d0d3f9bb41
refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals
2015-06-05 17:29:36 -07:00
Leonardo de Moura
af3f0088f4
feat(frontends/lean): add 'override' (notation) command
2015-05-20 11:42:16 -07:00
Leonardo de Moura
061e26157e
fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking
2015-05-08 12:41:23 -07:00
Leonardo de Moura
1a28a3c36f
feat(frontends/lean): add 'print inductive' command
2015-04-29 15:22:10 -07:00
Leonardo de Moura
6134c8822a
fix(frontends/lean/util): assertion violation
...
fixes #559
2015-04-24 15:09:23 -07:00
Leonardo de Moura
91f21c007a
feat(frontends/lean): remove 'context' command
2015-04-22 11:32:02 -07:00
Leonardo de Moura
52e9ad1a98
feat(frontends/lean): allow persistent notation declaration in sections (when they do not contain parameters)
...
see issue #554
2015-04-21 19:04:06 -07:00
Leonardo de Moura
9b577a7b3e
feat(frontends/lean): add 'migrate' command
2015-03-14 21:48:00 -07:00
Leonardo de Moura
fc3a7bac59
feat(frontends/lean): improve error handling inside match-with expressions
2015-03-13 23:25:46 -07:00
Leonardo de Moura
8240d7adcd
perf(frontends/lean/util): improve univ_metavars_to_params_fn
...
We moved to replace_visitor because it uses a more precise cache.
2015-03-02 18:25:00 -08:00
Leonardo de Moura
4248ad644d
fix(frontends/lean): priority expressions parser
2015-02-14 12:26:06 -08:00
Leonardo de Moura
014271da8b
feat(frontends/lean): better error messages for ill-terminated declarations
2015-02-10 14:38:00 -08:00
Leonardo de Moura
b5c4e603db
feat(frontends/lean): allow parameters to be used in sections
...
Restriction:
- coercions and notations cannot be defined in parametric sections
closes #401
2015-01-23 17:42:19 -08:00
Leonardo de Moura
a22dc773b7
refactor(frontends/lean): move some auxiliary procedures to library/tactic
2014-12-19 15:19:45 -08:00
Leonardo de Moura
0443c1e70c
fix(frontends/lean): intro tactic + universe variables, fixes #362
2014-12-03 12:56:30 -08:00
Leonardo de Moura
2281fb30c8
refactor(library): use "symbolic" precedences in the standard library
2014-11-29 19:08:37 -08:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
5d5fd2da50
fix(frontends/lean): tactic + section variables, fixes #332
2014-11-21 10:07:16 -08:00
Leonardo de Moura
3aac26d658
fix(frontends/lean): tactic + variables bug, fixes #315
2014-11-09 14:43:22 -08:00
Leonardo de Moura
efe1105eb9
fix(frontends/lean): alias generation for composite names was not working
...
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.
The commit also fix a bug in the generate of aliases for recursors
2014-11-03 15:43:58 -08:00
Leonardo de Moura
6107da05db
fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283
2014-10-29 19:47:14 -07:00
