Leonardo de Moura
210b7c8fb7
fix(library/tactic): fixes #1513
...
Implement rename tactic in Lean using revert/intro
2017-04-15 11:34:24 -07:00
Leonardo de Moura
fe0b694a06
feat(library/type_context): do not cache whnf in tmp_mode if term contains metavariables
2017-04-13 18:15:34 -07:00
Leonardo de Moura
7cc68130b3
feat(library/type_context): remove assign regular uvars hack
2017-04-13 18:15:29 -07:00
Sebastian Ullrich
8ea2bc08cb
feat(init/meta/interactive): add generalizing parameter to induction
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
17204f9629
feat(library/vm/interaction_state): capture tactic profile data if enabled
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
026c5ee509
fix(library/init/meta/expr,library/vm/vm_expr): fix macro args
2017-04-11 17:07:28 -07:00
Gabriel Ebner
cefc26d9cb
refactor(library/system/process): add exit status and working directory
2017-04-11 16:42:17 -07:00
Gabriel Ebner
acf75bd69b
fix(library/handle): handle double close
2017-04-11 16:42:17 -07:00
Gabriel Ebner
e2fa363423
feat(library/system/io,shell/lean): add --run switch
2017-04-11 16:41:30 -07:00
Gabriel Ebner
e1fae7b761
fix(library/module): correctly print kernel exceptions
2017-04-10 15:59:31 +02:00
Gabriel Ebner
01a7efc007
fix(library/module_mgr): do not crash on missing imports
...
Fixes #1506 .
2017-04-04 19:56:33 +02:00
Gabriel Ebner
c06bef0505
fix(library/aux_definition): also zeta expand the local context
...
@leodemoura The forced zeta-expansion in mk_aux_definition might
cause problems if we use tactic.abstract without zeta-reduction.
However, we never use the non-zeta mode, and it already fails right now
if you accidentally use zeta-expansion in the proof we want to abstract.
2017-04-04 09:04:37 +02:00
Sebastian Ullrich
7ac2f1be89
fix(util/name): segfault on name() == "foo"
...
Fixes #1505
2017-04-03 12:32:35 +02:00
Leonardo de Moura
a007c93280
feat(library/tactic/dsimplify): replace assigned metavariables
2017-04-02 12:49:29 -07:00
Leonardo de Moura
6dbf53f195
fix(library/type_context): fixes #1502
2017-04-02 12:49:06 -07:00
Gabriel Ebner
98fb21eab4
chore(frontends/lean/{parser_state,parser_pos_provider}): compiler warnings
2017-04-01 20:23:33 +02:00
Gabriel Ebner
cde946f293
fix(frontends/lean/scanner): fix assertion
2017-04-01 16:38:02 +02:00
Leonardo de Moura
b7c3d5a9f5
fix(frontends/lean/scanner): assertion
2017-03-31 19:39:13 -07:00
Leonardo de Moura
b42ae2cf54
fix(library/type_context): fixes #1500
2017-03-31 19:19:44 -07:00
Leonardo de Moura
6c68aeee01
feat(library/system/io): add io.iterate primitive
2017-03-31 11:34:09 -07:00
Sebastian Ullrich
3f98eb84c5
fix(library/print): consider constant roots in is_used_name
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
3f87755a2a
fix(frontends/lean/pp): qualify constant shadowed by local
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
669c4130b1
fix(frontends/lean/builtin_expr): no field notation after @/@@
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
cd013f22c0
chore(*): replace "'^.' notation" with "field notation", pretty print using "."
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
93fdfdc4b6
feat(frontends/lean/elaborator): better error message on field notation that was probably supposed to be a single ident
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
3c8e176fb0
fix(frontends/lean/interactive): fix info on new field notation
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
add8836ab2
fix(frontends/lean/{elaborator,parser}): use position of '.' for field notation position
...
Note that flycheck will still highlight the entire word...
2017-03-31 09:40:49 -07:00
Sebastian Ullrich
b92af074c0
feat(kernel/pos_info_provider): add save_pos_info
...
Allows the elaborator to contribute new info locations
2017-03-31 09:40:48 -07:00
Sebastian Ullrich
643d68e89a
fix(emacs/lean-type): use correct function for 'sticky' eldoc messages
2017-03-31 09:40:48 -07:00
Gabriel Ebner
f9c1ceb717
fix(frontends/lean/scanner): correctly handle positions in empty files
2017-03-31 09:40:15 -07:00
Leonardo de Moura
84bfd3e298
chore(frontends/lean): update keywords
...
Remark: "as" doesn't need to be a keyword.
So, we can now write patterns such as (a::as).
2017-03-30 16:51:08 -07:00
Leonardo de Moura
40481b89db
chore(emacs/lean-syntax): update
2017-03-30 16:47:44 -07:00
Kai Ruemmler
aa86eda214
fix(emacs/lean-server): define-fringe-bitmap is only defined in graphics mode
2017-03-30 11:19:10 -07:00
Gabriel Ebner
467e547160
fix(shell/CMakeLists): run all tests serially
2017-03-30 06:49:42 +02:00
Gabriel Ebner
3253a79e77
refactor(tests/lean/fail): use test suite runner
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
7a147eab12
fix(frontends/lean/decl_util): truly fix top-level do pattern names race
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
b2dfae8a67
chore(tests/lean/caching_user_attribute): fix flaky test
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
678044d1d6
refactor(shell/lean): use log tree node from module_info
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
e7f01b7490
fix(frontends/lean/decl_util): bad reset in scope destructor
2017-03-30 06:04:00 +02:00
Sebastian Ullrich
4a33045b84
chore(tests/lean,shell/lean): run leantests and leanruntests in parallel
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
Jared Roesch
dc4086d0ed
feat(library/vm/process): add basic process support
2017-03-28 18:08:06 -07:00
Leonardo de Moura
1ffc01f1d5
chore(tests/frontends/lean/lean_scanner): fix test
2017-03-28 18:00:19 -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
