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
Leonardo de Moura
9721757d87
fix(frontends/lean/builtin_exprs): position information when parsing do-notation
2016-07-22 11:14:33 -07:00
Leonardo de Moura
9740515be1
chore(frontends/lean/builtin_exprs): remove '#tactic'
2016-07-02 11:15:46 +01:00
Leonardo de Moura
6cb63d5f9a
feat(frontends/lean/builtin_exprs): simplify '@' and '@@'
2016-07-02 11:08:18 +01:00
Leonardo de Moura
90d920b7c9
chore(frontends/lean,library/explicit): remove dead code
2016-07-02 01:57:43 +01:00
Leonardo de Moura
97719a4c5f
refactor(frontends/lean): disable '!' operator, and adjust standard library
2016-07-02 01:41:46 +01:00
Leonardo de Moura
fbec9053dc
feat(frontends/lean/builtin_exprs): add 'else case' for do-match notation
2016-06-27 15:28:17 +01:00
Leonardo de Moura
c624c2d932
feat(frontends/lean): allow patterns in 'do' notation
2016-06-24 19:28:48 -07:00
Leonardo de Moura
9de819baaf
chore(library/init/monad): change precedence for >>= and >>
...
We are now using the same one used in Haskell.
2016-06-21 18:29:07 -07:00
Leonardo de Moura
46cf91c969
chore(frontends/lean): remove 'assert' keyword
...
In Lean3, `assert` was just an alias for `have`.
2016-06-17 14:20:26 -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
d16e1d85fb
chore(frontends/lean): remove proof-qed expressions
2016-06-13 10:04:51 -07:00
Leonardo de Moura
0261a81eb0
feat(frontends/lean): add '()' as notation for unit.star
2016-06-08 17:26:48 -07:00
Leonardo de Moura
a61a6abba1
feat(src/frontends/lean/builtin_exprs): allow user to specify type of local decls in 'do' notation
2016-06-06 14:44:57 -07:00
Sebastian Ullrich
9561b45af1
fix(frontends/lean): uniform handling of declaration compound names
...
* allow compound names in `namespace` and `structure`
* adjust error messages
Conflicts:
src/frontends/lean/builtin_tactics.cpp
2016-06-02 18:13:50 -07:00
Leonardo de Moura
7c97d88be5
feat(frontends/lean/builtin_exprs): add optional curly braces for do-notation
2016-05-25 15:15:39 -07:00
Leonardo de Moura
174fba9dbd
feat(frontends/lean): add support for monadic 'do'-notation
2016-05-24 17:18:15 -07:00
Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -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
de64750621
chore(frontends/lean): disable expressions that use tactic framework
2016-04-25 15:07:26 -07:00
Leonardo de Moura
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -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
f55e456c84
chore(*): remove remaining references to by+ and begin+
2016-02-29 13:59:06 -08:00
Leonardo de Moura
b7b4b6d838
chore(src/frontends/lean/builtin_exprs): remove unnecessary parameter
2016-02-29 13:57:18 -08:00
Leonardo de Moura
fbe5188480
refactor(frontends/lean): remove 'by+' and 'begin+' tokens
2016-02-29 13:45:43 -08:00
Leonardo de Moura
bf60999ede
fix(frontends/lean/builtin_exprs): 'using' expression
2016-02-29 13:23:39 -08:00
Leonardo de Moura
2b1d734544
feat(kernel/expr): remove 'contextual' flag from binder_info
2016-02-29 12:41:43 -08:00
Leonardo de Moura
b41c65f549
feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking
2016-02-29 12:31:23 -08:00
Leonardo de Moura
101cf1ec4c
feat(frontends/lean): remove difference between 'have' and 'assert'
2016-02-29 11:28:20 -08:00
