Leonardo de Moura
f02de7e380
feat(frontends/lean/builtin_exprs): curly braces after show/have enter interactive mode
2016-11-18 17:00:08 -08:00
Leonardo de Moura
b59c10118d
fix(*): memory leaks
2016-11-11 11:56:54 -08:00
Leonardo de Moura
93ccea11fc
chore(frontends/lean): remove dead code
...
`abstract` can be implemented as a tactic on top of add_decl.
2016-11-04 12:36:12 -07:00
Leonardo de Moura
9b84db083d
fix(frontends/lean): error localization bugs
2016-10-15 13:40:57 -07:00
Leonardo de Moura
837915f06b
fix(frontends/lean/builtin_exprs): bug when parsing in quoted names
2016-10-01 13:19:24 -07:00
Leonardo de Moura
7ab12ed57f
feat(library/init/algebra): improve transport_to_additive (copy attributes)
2016-10-01 12:55:17 -07:00
Leonardo de Moura
051b6bd026
feat(frontends/lean/tactic_notation): add notation for entering auto-quotation mode
2016-09-30 16:18:52 -07:00
Leonardo de Moura
c8a720212b
feat(frontends/lean): 'by' is now also using interactive mode syntax
2016-09-29 01:57:40 -07:00
Leonardo de Moura
bbf21b4e65
feat(frontends/lean/begin_end_block): auto-quote identifiers
2016-09-25 17:25:21 -07:00
Leonardo de Moura
97261fcc48
feat(frontends/lean): add very basic 'begin ... end' block support
2016-09-24 21:27:27 -07:00
Leonardo de Moura
93106a6b02
chore(frontends/lean/builtin_exprs): error message consistency
2016-09-23 10:08:22 -07:00
Leonardo de Moura
7ae778e925
feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>'
2016-09-23 08:18:19 -07:00
Leonardo de Moura
b55a17614a
feat(frontends/lean): structure instances
2016-09-21 22:52:43 -07:00
Leonardo de Moura
c0ff9967af
feat(frontends/lean): add basic notation for collections
2016-09-21 16:20:57 -07:00
Leonardo de Moura
dde5f7ac70
feat(frontends/lean): add aliases such as: .1 for ~>1
2016-09-21 11:32:02 -07:00
Leonardo de Moura
b67216374c
feat(frontends/lean): projection notation
2016-09-21 11:14:41 -07:00
Leonardo de Moura
8657230435
chore(frontends/lean): new token for projections, and cleanup
2016-09-21 10:18:49 -07:00
Leonardo de Moura
318ef761d3
feat(frontends/lean): lambda+anonymous_constructor+match notation
2016-09-21 08:49:05 -07:00
Leonardo de Moura
335242e9f1
chore(frontends/lean): remove info_annotation module
2016-09-19 21:19:31 -07:00
Leonardo de Moura
09687f70af
chore(frontends/lean/builtin_exprs): fix compilation warning
2016-09-19 19:50:30 -07:00
Leonardo de Moura
2a069a4d2a
chore(frontends/lean): remove server and info_manager
2016-09-19 18:44:03 -07:00
Leonardo de Moura
9f1a576e98
chore(frontends/lean): remove dead code from parser
2016-09-19 17:04:59 -07:00
Leonardo de Moura
5e4e1ba88a
chore(frontends/lean): delete old definition command
2016-09-19 16:50:25 -07:00
Leonardo de Moura
4e0e812811
fix(frontends/lean/builtin_exprs): patterns in do-notation
2016-09-18 18:19:51 -07:00
Leonardo de Moura
90bfd84a07
feat(frontends/lean): Type is now (Type 1)
...
In the standard library, we should use explicit universe variables for
universe polymorphic definitions.
Users that want to declare universe polymorphic definitions but do not
want to provide universe level parameters should use
Type _
or
Type*
2016-09-17 14:30:54 -07:00
Leonardo de Moura
5e8f2add84
refactor(library/init): use universe variables
2016-09-17 12:25:02 -07:00
Leonardo de Moura
0b90ace9f8
feat(frontends/lean/builtin_exprs): basic support for let-expr with patterns
2016-09-11 22:21:10 -07:00
Leonardo de Moura
1afd81384f
chore(library/let): delete let-macro hack
2016-09-10 13:06:07 -07:00
Leonardo de Moura
91994ff823
feat(frontends/lean/elaborator): switch to new let-decls
2016-09-10 13:00:53 -07:00
Leonardo de Moura
b12fa5c8da
feat(frontends/lean): add support for 'suffices'-expression in the new elaborator
2016-09-08 17:26:27 -07:00
Leonardo de Moura
001991dbeb
feat(frontends/lean): use equations_header
2016-08-30 13:45:59 -07:00
Leonardo de Moura
e99eb6d47e
feat(frontends/lean): revising inaccessible terms syntax again :(
2016-08-19 13:57:12 -07:00
Leonardo de Moura
e384b5c5f9
refactor(frontends/lean): move structure_instance to separate module
2016-08-16 14:56:09 -07:00
Leonardo de Moura
fc4e304b27
refactor(library): move equations to equations_compiler
2016-08-11 10:08:30 -07:00
Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
Leonardo de Moura
f5c35f8d76
chore(*): fix compilation warnings
2016-08-10 18:03:13 -07:00
Leonardo de Moura
f75de2e950
chore(library/definitional,frontends/lean): remove decreasing macro
2016-08-09 16:27:33 -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
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
5eddff44ab
fix(frontends/lean/builtin_exprs): better error position
2016-08-06 13:43:09 -07:00
Leonardo de Moura
b6420904f5
feat(frontends/lean): resolved quoted names
2016-08-05 17:04:36 -07:00
Leonardo de Moura
8b05fba6ef
feat(frontends/lean/elaborator): propagate expected type to arguments when elaborating constructors
2016-08-04 14:07:15 -07:00
Leonardo de Moura
6a0d9dab40
feat(frontends/lean/elaborator): anonymous constructors
2016-08-04 13:03:49 -07:00
Leonardo de Moura
1ca15e9b42
chore(frontends/lean): remove obtain-expr dead code
2016-08-03 17:41:16 -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
7ddf1e817b
chore(frontends/lean): coercions are disabled by default
2016-07-29 13:03:23 -07:00
Leonardo de Moura
477a137db9
feat(frontends/lean): remove 'using' expressions
...
Reason: we have include/omit commands
2016-07-28 09:53:27 -07:00
Leonardo de Moura
01283512a6
feat(frontends/lean/elaborator): add code for deciding which function application elaboration procedure should be used
2016-07-25 12:55:28 -07:00
Leonardo de Moura
212d222047
feat(frontends/lean): quoted names
2016-07-22 19:06:57 -07:00
Leonardo de Moura
599916c352
fix(frontends/lean/builtin_exprs): position information
2016-07-22 11:22:37 -07:00
