Sebastian Ullrich
|
e7f01b7490
|
fix(frontends/lean/decl_util): bad reset in scope destructor
|
2017-03-30 06:04:00 +02:00 |
|
Leonardo de Moura
|
ad859817b1
|
feat(frontends/lean): allow local decls to shadow namespaces
|
2017-03-29 16:09:45 -07:00 |
|
Leonardo de Moura
|
cb049f42b7
|
fix(frontends/lean/elaborator): resolve_local_name
|
2017-03-28 17:57:13 -07:00 |
|
Leonardo de Moura
|
71685e4dd6
|
feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term
Replace `^.` with `.` in the stdlib
|
2017-03-28 17:47:49 -07:00 |
|
Leonardo de Moura
|
4fa3d31c95
|
fix(frontends/lean/elaborator): as_atomic at resolve_local_name
|
2017-03-28 16:21:14 -07:00 |
|
Leonardo de Moura
|
87932f1c56
|
feat(frontends/lean): change notation for inaccessible patterns
The following are accepted
.(t)
._
We don't accept .t anymore because it will conflict with the field
access notation.
|
2017-03-28 16:09:15 -07:00 |
|
Leonardo de Moura
|
6183c7676e
|
feat(frontends/lean): use . for field access
|
2017-03-28 15:29:54 -07:00 |
|
Leonardo de Moura
|
8e2dcb8ad8
|
chore(frontends/lean): remove ^. variants (~> and ↣)
This modification was motivated by a discussion at slack.
|
2017-03-28 12:23:33 -07:00 |
|
Leonardo de Moura
|
cefe1dd294
|
chore(frontends/lean/parser): update comments
|
2017-03-28 12:10:11 -07:00 |
|
Leonardo de Moura
|
092985f777
|
fix(frontends/lean/util): fixes #1495
We should freeze only constants
|
2017-03-28 11:55:11 -07:00 |
|
Leonardo de Moura
|
07c29c0779
|
chore(library/abstract_parser,frontends/lean/parser): remove dead code
|
2017-03-28 11:51:50 -07:00 |
|
Leonardo de Moura
|
9a4e04b8ca
|
feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values
|
2017-03-27 21:37:31 -07:00 |
|
Leonardo de Moura
|
71bf0bcc5d
|
fix(frontends/lean/builtin_exprs): fixes #1493
|
2017-03-27 17:57:13 -07:00 |
|
Sebastian Ullrich
|
68c1ff6219
|
feat(frontends/lean/builtin_exprs): use local field inference for info too
|
2017-03-27 14:01:38 -07:00 |
|
Sebastian Ullrich
|
00cb784bd8
|
fix(frontends/lean/builtin_exprs): do not hide elaborated field info when local inference fails
|
2017-03-27 14:01:29 -07:00 |
|
Sebastian Ullrich
|
e63c1d3347
|
refactor(frontends/lean/info_manager): use pos_info
|
2017-03-27 14:01:19 -07:00 |
|
Gabriel Ebner
|
318910f99b
|
refactor(frontends/lean/parser): store snapshots in a lazy async list
|
2017-03-27 14:00:53 -07:00 |
|
Sebastian Ullrich
|
55425e7b1f
|
fix(frontends/lean/structure_cmd): unfold untrusted macros in intro rules
|
2017-03-27 13:42:08 -07:00 |
|
Leonardo de Moura
|
e98f69d1ac
|
fix(frontends/lean/elaborator): ignore auto/default params when @ is used
see #1485
@kha We need this commit to be able to execute commands such as:
```lean
#check @monad.mk
```
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
bf8292cb17
|
feat(frontends/lean/structure_cmd): allow local notations
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
3aaf64d06f
|
feat(frontends/lean/elaborator): elaborate auto params and explicitly given fields as soon as possible, too.
Also make sure not to elaborate fields before other fields their type depends on.
Makes inline tactic proofs in structure instances possible.
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
3851009ea3
|
fix(frontends/lean/elaborator): elaborate auto_param fields last
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
d8eef9e68e
|
feat(frontends/lean/util): allow lazily resolved auto params
|
2017-03-27 13:42:08 -07:00 |
|
Leonardo de Moura
|
900c56be05
|
feat(frontends/lean,library/equations_compiler): abstract proofs in equations and regular definitions
|
2017-03-25 14:22:52 -07:00 |
|
Gabriel Ebner
|
2c7b6fc48f
|
fix(frontends/lean/parser): only show sorry warning once per import
|
2017-03-24 09:19:17 +01:00 |
|
Gabriel Ebner
|
7442aa0752
|
fix(frontends/lean/parser): better task description
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
c55579dd69
|
fix(frontends/lean/scanner): initialize m_pos
|
2017-03-24 07:04:35 +01:00 |
|
Leonardo de Moura
|
527c8851a8
|
refactor(library/system/io): use type classes
|
2017-03-23 14:29:07 -07:00 |
|
Gabriel Ebner
|
a6f7f31e85
|
refactor(shell,emacs): handle different checking modes in server
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a8ba78e20a
|
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
|
2017-03-23 09:07:08 +01:00 |
|
Gabriel Ebner
|
9dfd8e1018
|
fix(shell/server): fix field completion
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
c7ca21625c
|
feat(util/log_tree): annotate nodes with detail levels
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
098d6f8f2a
|
refactor(init/meta/tactic): remove report_errors argument from to_expr
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
c8fff9f4ff
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
Gabriel Ebner
|
98f86ccabd
|
chore(frontends/lean/parser): remove obsolete option
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
c5c0a74d77
|
fix(frontends/lean/definition_cmds): reinstate fallback to sorry
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
667d06108a
|
chore(*): fix clang warnings
|
2017-03-23 09:00:58 +01:00 |
|
Gabriel Ebner
|
2799375d24
|
chore(*): style
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
26ba9c23a7
|
refactor(util/task): add eager execution
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
3eba8d3ffc
|
refactor(util/task): do not propagate errors
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
aebd18f136
|
feat(shell/server): only compile region of interest
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
5f872912e0
|
refactor(shell/lean): set exit status 1 iff at least one error was reported
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
595cbb8fe9
|
refactor(*): task<T>, log_tree, cancellation_token
|
2017-03-23 08:57:52 +01:00 |
|
Leonardo de Moura
|
60dd85719c
|
feat(library/system/io): system.io without axioms
|
2017-03-22 23:36:05 -07:00 |
|
Leonardo de Moura
|
e6c5ba29d6
|
fix(library/message_builder): remove unnecessary field
see #1473
|
2017-03-22 08:23:29 -07:00 |
|
Sebastian Ullrich
|
da7e21696e
|
feat(init/meta/interactive): rw goal info on ,
|
2017-03-22 07:54:12 -07:00 |
|
Sebastian Ullrich
|
524a381f22
|
refactor(lean/tactic_notation): better goal info tweak on ,
|
2017-03-22 07:54:12 -07:00 |
|
Sebastian Ullrich
|
f9854be13f
|
feat(frontends/lean/parser): save id info for non-overloaded constants
|
2017-03-22 07:35:14 -07:00 |
|
Sebastian Ullrich
|
897b4f9db1
|
fix(frontends/lean/builtin_exprs): override scope behavior for strict quoted names
|
2017-03-22 07:34:50 -07:00 |
|
Leonardo de Moura
|
3a878bd3f4
|
fix(frontends/lean/interactive): compilation warning with older versions of g++
|
2017-03-21 08:31:16 -07:00 |
|