Leonardo de Moura
|
494e5b65c5
|
feat(library/init/meta/tactic): add apply_auto_param and apply_opt_param tactics
see #1485
|
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 |
|
Leonardo de Moura
|
70e6c380ed
|
fix(library/vm/vm_io): fix io_monad
see #1485
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
9e8ef54402
|
refactor(init/data/list/instances): simplify proofs
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
b3a0eb9bfc
|
fix(init/meta/interactive): mk_simp_set: also remove equational lemmas
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
c7b47c7b7f
|
fix(system/io): try to fix io monad
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
83511bdae1
|
feat(library/tactic/elaborator_exception): show context of failed placeholders
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
dfd84666e2
|
feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances
|
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
|
b51e666bda
|
feat(init/category/monad): simplify monad.seq._default
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
3ead6be9ca
|
feat(init): add default value proofs to the monadic hierarchy
|
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 |
|
Leonardo de Moura
|
0890ae5c01
|
fix(library/type_context): When synthesizing subsingleton instances, we should not assign universe metavariables
fixes #1487
|
2017-03-25 10:54:12 -07:00 |
|
Gabriel Ebner
|
122355aa32
|
fix(emacs/lean-server): emacs 24 compatibility
|
2017-03-24 08:28:32 -07:00 |
|
Gabriel Ebner
|
69f0d30452
|
fix(emacs/lean-server): update roi when user changes checking mode
|
2017-03-24 09:29:06 +01: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
|
e784fad8c6
|
feat(shell/server,emacs): add visible lines and above checking mode
|
2017-03-24 09:08:17 +01:00 |
|
Gabriel Ebner
|
33b55250a8
|
fix(emacs/lean-server): fix highlight pending tasks toggle
|
2017-03-24 07:35:14 +01:00 |
|
Gabriel Ebner
|
9db6d1d845
|
perf(emacs/lean-server): only render visible task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
f16c2c68db
|
perf(emacs/lean-server): speed up task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
83c4b410be
|
feat(emacs/lean-server): more awesome fringe highlighting
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
7442aa0752
|
fix(frontends/lean/parser): better task description
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
24e19bdd00
|
feat(emacs): add tooltip to task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
af588add56
|
fix(emacs/lean-server): correctly react to scrolling
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
34586a2e82
|
feat(util/log_tree): deindent _next nodes
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
fdd80c12dd
|
feat(util/log_tree): inherit description
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
c55579dd69
|
fix(frontends/lean/scanner): initialize m_pos
|
2017-03-24 07:04:35 +01:00 |
|
Leonardo de Moura
|
7543d9e050
|
chore(tests/lean/io_fs_error): fix test
|
2017-03-23 18:52:37 -07:00 |
|
Leonardo de Moura
|
8cf43e1b30
|
feat(library/tactic/tactic_state): add tactic.run_io
|
2017-03-23 18:17:53 -07:00 |
|
Leonardo de Moura
|
7db44ce403
|
chore(library/vm/vm_io): style
|
2017-03-23 16:58:28 -07:00 |
|
Leonardo de Moura
|
fe3875a103
|
feat(library/system/io): add stdin, stdout and stderr
|
2017-03-23 16:49:39 -07:00 |
|
Leonardo de Moura
|
82748a61b7
|
feat(library/system/io): basic file system API
|
2017-03-23 16:30:16 -07:00 |
|
Leonardo de Moura
|
527c8851a8
|
refactor(library/system/io): use type classes
|
2017-03-23 14:29:07 -07:00 |
|
Leonardo de Moura
|
ccd9a8212a
|
chore(shell/lean_js): compilation warning
|
2017-03-23 12:56:35 -07:00 |
|
Gabriel Ebner
|
0d4f829ada
|
fix(library/mt_task_queue): fix abort
|
2017-03-23 15:37:52 +01:00 |
|
Gabriel Ebner
|
8814fe8276
|
chore(tests/lean): add test for error position clamping
|
2017-03-23 09:23:57 +01:00 |
|
Gabriel Ebner
|
69322cd523
|
fix(util/task): evaluate dependencies iteratively
|
2017-03-23 09:16:49 +01:00 |
|
Gabriel Ebner
|
2da9d72491
|
chore(tests/lean/interactive): fix test
|
2017-03-23 09:14:32 +01:00 |
|
Gabriel Ebner
|
73826eee54
|
chore(util/rb_tree): fix clang warning
|
2017-03-23 09:07:50 +01:00 |
|
Gabriel Ebner
|
14c24a66a1
|
feat(emacs): provide commands to change check mode
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a6f7f31e85
|
refactor(shell,emacs): handle different checking modes in server
|
2017-03-23 09:07:09 +01:00 |
|
Sebastian Ullrich
|
1f07319bc7
|
fix(emacs/lean-server): Emacs 24 compatibility
|
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
|
d90dda01b0
|
chore(*): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
9dfd8e1018
|
fix(shell/server): fix field completion
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
5e29fe227e
|
fix(shell/server): set global ios in info and complete tasks
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
dfb5dad1a3
|
chore(util/log_tree): style
|
2017-03-23 09:03:43 +01:00 |
|