Gabriel Ebner
a24490a06a
fix(emacs/lean-server): wrap correct function with save-match-data
...
In emacs 24, apparently just setting a timer changed the match data...
2016-12-11 11:17:28 -08:00
Leonardo de Moura
c8d6836aa1
feat(library): port nat sub lemmas
2016-12-11 09:46:45 -08:00
Gabriel Ebner
f8479762a1
fix(emacs/lean-server): make sure all timers are wrapped in save-match-data
2016-12-11 08:30:00 -08:00
Leonardo de Moura
18098e9455
perf(library/init/data/list/basic): avoid naive quadratic implementations
2016-12-10 13:18:11 -08:00
Leonardo de Moura
aba6f8b8a8
feat(frontends/lean/parser): add support for anonymous parameters
...
Example:
check λ _, 0
2016-12-10 11:07:58 -08:00
Leonardo de Moura
9f6e71b374
feat(library/tactic): add "approximate" parameter to apply_core and rewrite_core
...
If this parameter is set to true, then approximate unification is
used.
closes #1208
2016-12-10 10:24:05 -08:00
Jeremy Avigad
0950b7a49f
feat(library/init/meta/interactive): allow cases on an arbitrary expression
2016-12-10 09:54:03 -08:00
Jeremy Avigad
1dd91c6e6a
feat(library/init/meta/interactive): add fapply
2016-12-10 09:53:53 -08:00
Jeremy Avigad
1ba55e5cda
feat(library/init/meta/interactive): allow metavariable in change tactic
2016-12-10 09:53:36 -08:00
Leonardo de Moura
55401a95ec
fix(frontends/lean/parser): scope in tactic mode
2016-12-10 09:39:13 -08:00
Gabriel Ebner
e03c31d2f9
refactor(gitignore): remove old ignore entries
2016-12-10 08:42:39 -08:00
Gabriel Ebner
09fa1298ce
fix(gitignore): ignore autosave files
2016-12-10 08:42:29 -08:00
Gabriel Ebner
872082bdd9
chore(*): remove emacs autosave file
2016-12-10 08:42:20 -08:00
Leonardo de Moura
b5dc88ee37
fix(library/equations_compiler/elim_match): see #1216
...
Fixes the problem described at #1216 .
This is an alternative fix that prevents the m_var_stack from being in
an inconsistent state.
2016-12-08 15:38:14 -08:00
Jeremy Avigad
7155e8114b
refactor(src/emacs/*): remove dependence on fill-column-indicator
2016-12-08 14:53:09 -08:00
Leonardo de Moura
692701c5ef
feat(library/init/meta): use cheap "reflexivity" after simp and rewrite
...
The idea is to make sure lean doesn't timeout (at reflexivity) when we apply simp or
rewrite in goals such as
(x y : nat) |- x + y + 10000000000 = x + y + 200000000000000
This commit also addresses an issue raised at #1218
2016-12-08 14:41:26 -08:00
Leonardo de Moura
0818b02eb3
test(tests/lean/run): add test for @1218
2016-12-08 14:10:47 -08:00
Daniel Selsam
aed6d8fea0
fix(tactic/dsimplify.cpp): must whnf in post to be idempotent
2016-12-08 13:34:32 -08:00
Jeremy Avigad
6f64244f2a
refactor(library/init/meta/tactic): switch 'pose' and 'note'
2016-12-08 13:17:42 -08:00
Gabriel Ebner
2867163db0
fix(tests): initialize util module
2016-12-08 13:11:53 -08:00
Gabriel Ebner
51821bd8c9
fix(util/thread): do not initialize thread_finalizers_manager in multiple threads
2016-12-08 13:11:40 -08:00
Leonardo de Moura
275cfeac1a
fix(library/type_context): incorrect assertion
2016-12-08 12:58:10 -08:00
Leonardo de Moura
09ed8e1136
fix(library/type_context): compilation error in debug mode
2016-12-08 12:49:04 -08:00
Leonardo de Moura
6577cc87a3
feat(library): add pre_monad
...
closes #1235
2016-12-08 12:48:55 -08:00
Leonardo de Moura
9222c89198
chore(tests/lean/dunfold_constant): fix test output
2016-12-08 11:34:08 -08:00
Leonardo de Moura
eb0b158ad1
chore(tests/lean/test_single): remove tmp files
2016-12-08 11:33:54 -08:00
Daniel Selsam
f952dbc78e
fix(init/meta/expr.lean): is_app_of can return true for constants as well
2016-12-08 11:23:53 -08:00
Leonardo de Moura
079a442404
feat(library/type_context): add option for controlling threshold for applying offset constraints
2016-12-08 11:21:05 -08:00
Leonardo de Moura
be3cff0c46
feat(library/type_context): move offset constraint resolution to lazy delta loop
2016-12-08 11:00:15 -08:00
Gabriel Ebner
bcc92af237
fix(emacs/load-lean): require unicode-fonts package
2016-12-08 10:44:47 -08:00
Leonardo de Moura
e80eccdd60
chore(library/st_task_queue): style
2016-12-08 10:43:39 -08:00
Leonardo de Moura
e01c7bfef5
chore(frontends/lean/definition_cmds): update comment
2016-12-08 10:35:32 -08:00
Gabriel Ebner
716502c502
fix(library/st_task_queue): check dependencies on task submission
2016-12-08 10:32:37 -08:00
Leonardo de Moura
e13bac41c3
fix(frontends/lean): 'sorry' axiom auto generation
2016-12-08 10:31:52 -08:00
Leonardo de Moura
7bffcf776b
chore(library/mt_task_queue, library/task_queue): style
2016-12-08 09:26:22 -08:00
Daniel Selsam
6120f8cc9f
fix(src/library/tactic/simplify): relaxed_whnf when checking if fn is dependent
2016-12-08 07:41:42 -08:00
Leonardo de Moura
b9de2fda0c
chore(library/init/algebra/order): remove unnecessary *.refl lemmas
2016-12-08 07:32:25 -08:00
Leonardo de Moura
023f216cab
chore(init/algebra/order): use new attribute syntax
2016-12-08 07:22:58 -08:00
Jeremy Avigad
281903edee
refactor(library/init/data/nat/lemmas): better name for self_lt_succ
2016-12-08 07:20:39 -08:00
Jeremy Avigad
16b239cbff
feat(library/init/algebra/order): add refl and trans attribute and dot notation
2016-12-08 07:20:22 -08:00
Jeremy Avigad
9c6605c992
refator(library/init/data/set): make implicit argument in subset weak
2016-12-08 07:20:12 -08:00
Jeremy Avigad
814da88858
refactor(library/init/data/nat/basic,lemmas): alternative name, and rename le.elim to le.dest
2016-12-08 07:20:02 -08:00
Jeremy Avigad
acb58e8a87
feat(library/init/algebra/group,ring): alternative names for calculation lemmas
2016-12-08 07:19:41 -08:00
Jeremy Avigad
da6dfa6fdd
feat(library/init/logic): alternative theorem names, and make some arguments explicit
2016-12-08 07:19:38 -08:00
Leonardo de Moura
7b63d6566f
fix(util/dynamic_library): throwing exception inside destructor may crash application
2016-12-08 07:16:43 -08:00
Gabriel Ebner
5ee7076ae9
fix(emacs): update readme
2016-12-08 07:14:55 -08:00
Gabriel Ebner
60f0f30c5c
fix(tests/shared/thread): fix single-threaded build
2016-12-08 07:13:48 -08:00
Gabriel Ebner
bd69544663
fix(emacs/lean-server): start server in the directory of the file
2016-12-06 17:45:12 -08:00
Leonardo de Moura
58768940e3
chore(shell/server): std::make_unique is a C++14 feature
...
I got a compilation error
2016-12-06 17:22:24 -08:00
Gabriel Ebner
45d0525e52
feat(shell,emacs): new lean server protocol
2016-12-06 17:14:29 -08:00
