Leonardo de Moura
1cee5fbfea
chore(library/compiler/vm_compiler): hide API
2016-11-05 14:11:21 -07:00
Leonardo de Moura
c9da2f2542
chore(tests/lean): fix tests
2016-11-05 11:51:29 -07:00
Leonardo de Moura
b9afbf0aa8
test(tests/lean/run): add test for additive fragment
2016-11-05 11:47:43 -07:00
Leonardo de Moura
2d86d88c92
feat(library/tactic/user_attribute): allow user to specify whether attribute is persistent or not
2016-11-05 11:46:04 -07:00
Leonardo de Moura
43aa6eb87f
fix(library/class): bug in whnf_pred predicate
2016-11-05 11:44:05 -07:00
Leonardo de Moura
a551de8f36
doc(*): remove Lua from the list of required packages
2016-11-04 14:05:05 -07:00
Leonardo de Moura
93ccea11fc
chore(frontends/lean): remove dead code
...
`abstract` can be implemented as a tactic on top of add_decl.
2016-11-04 12:36:12 -07:00
Leonardo de Moura
ecb563baa3
chore(library/fun_info): patch assertion
...
The fixed assertion makes sure we don't get an array-index-out-of-bounds
in the for-loop in the end of the procedure.
2016-11-04 10:14:00 -07:00
Daniel Selsam
f3dc41b631
fix(library/tactic/simplify): only use auto_eq_congr if number of args match
2016-11-04 10:13:02 -07:00
Leonardo de Moura
1dcc21525a
chore(library/vm/vm): style
2016-11-04 09:55:20 -07:00
Gabriel Ebner
1aacf1f20b
chore(*): fix style errors
2016-11-04 09:47:17 -07:00
Gabriel Ebner
3f85253dac
fix(CMakeLists): uncomment style check
2016-11-04 09:47:17 -07:00
Gabriel Ebner
41643d6400
fix(library/compiler/vm_compiler): prevent segfault
2016-11-04 09:47:17 -07:00
Leonardo de Moura
5075891f66
chore(library/vm/vm): fix gcc 4.8 warning
2016-11-04 09:46:16 -07:00
Gabriel Ebner
ef1fc9871b
feat(library/vm/vm): profiler: show cumulative runtimes
2016-11-04 09:39:12 -07:00
Sebastian Ullrich
395ddd9d38
fix(frontends/lean/builtin_cmds): fix positioning of vm_eval output
2016-11-04 09:36:55 -07:00
Sebastian Ullrich
eb599481b9
fix(frontends/lean/parser): fix spurious "uses 'sorry'" messages
2016-11-04 09:36:55 -07:00
Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Leonardo de Moura
6173d95d18
feat(library/module,frontends/lean): store line/column number information
2016-11-02 16:55:21 -07:00
Leonardo de Moura
3212d9c83a
fix(library/module): store .olean file where inductive datatype was defined
2016-11-02 16:07:36 -07:00
Leonardo de Moura
cea572a167
feat(library/module): store .olean file name for imported declarations
2016-11-02 15:37:33 -07:00
Leonardo de Moura
3958d8485a
chore(library/module): remove dead code
2016-11-02 15:02:49 -07:00
Leonardo de Moura
9d3aa5b627
fix(library/compiler/elim_recursors): bug in elim_recursors
...
We may fail to type check auxiliary definitions that use rec_fn_macro.
The problem is that this macro cannot be unfolded.
So, we fix the problem by not type checking them. We add them as
constants, and store the definition in an auxiliary vector.
2016-11-02 14:19:28 -07:00
Leonardo de Moura
e62810c9b8
fix(library/compiler/lambda_lifting): make sure constructors are eta-expanded
...
closes #1133
2016-11-02 13:26:15 -07:00
Leonardo de Moura
30ae8a29b6
fix(library/compiler/elim_recursors): some recursor applications were not being eliminated
2016-11-02 13:05:52 -07:00
Daniel Selsam
05add2ea02
fix(library/tactic/simplify.cpp): fix debug tracing names
2016-11-02 10:23:38 -07:00
Leonardo de Moura
b22192eee1
fix(library/equations_compiler/elim_match): fixes #1171
...
We should not use value-transition (based on if-then-else) when there
are dependencies.
2016-10-31 17:42:39 +08:00
Gabriel Ebner
08f7e56b66
fix(vim/syntax): update to lean 3 syntax
2016-10-30 08:42:05 +08:00
Gabriel Ebner
1227e01dd2
fix(emacs): faster lean-info updates
2016-10-30 08:42:05 +08:00
Gabriel Ebner
e18370585d
fix(frontends/lean/server): fix relative dependency lookups
2016-10-30 08:42:05 +08:00
Gabriel Ebner
7cff9c4498
fix(emacs): clear error messages in next-error-mode
2016-10-30 08:42:05 +08:00
Gabriel Ebner
d071594b8e
refactor(emacs): use lean info buffer for next-error-mode
2016-10-30 08:42:05 +08:00
Gabriel Ebner
7d5c20c885
fix(emacs): show "no goal found" message in same buffer as goals
2016-10-30 08:42:05 +08:00
Leonardo de Moura
a77e4b5abf
fix(library/compiler/erase_irrelevant): bug at is_comp_irrelevant
2016-10-27 11:51:37 +08:00
Leonardo de Moura
ea3adf4a7c
feat(library/init/meta/tactic): universe polymorphic tactics
2016-10-25 03:42:55 +08:00
Leonardo de Moura
e358a15dd4
fix(frontends/lean/elaborator): show-goal-at-pos after last tactic
...
See issue #1169
2016-10-25 02:40:24 +08:00
Gabriel Ebner
5f803c0353
feat(frontends/lean/elaborator): make show-goal-at-pos work on
...
by-tactics
2016-10-21 15:42:29 -07:00
Gabriel Ebner
1c8b4515be
chore(emacs): fix cask warnings
2016-10-21 15:42:29 -07:00
Gabriel Ebner
9a175b9b19
chore(emacs): remove unused code
2016-10-21 15:42:29 -07:00
Gabriel Ebner
e6f75f2e0f
feat(shell/server,emacs/lean-mode): show-goal-at-pos
2016-10-21 15:42:29 -07:00
Gabriel Ebner
3833a60b7c
fix(emacs/lean-server): recognize error messages
2016-10-21 15:42:29 -07:00
Gabriel Ebner
47e6fd091f
refactor(frontends/lean): implement show goal function using exceptions
2016-10-21 15:42:29 -07:00
Leonardo de Moura
fa3475fa66
fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode
...
This commit also removes a "hack" that tried to fix this problem for
universe meta-variables only. Moreover, the hack was incomplete, since
it would not consider nested metavars.
2016-10-21 13:33:07 -07:00
Leonardo de Moura
a9fe684f26
chore(library/tactic/simplify): fix warning in release mode
2016-10-21 13:28:12 -07:00
Leonardo de Moura
2da0b1398c
chore(emacs/lean-company): disable async auto-completion
2016-10-19 19:47:57 -07:00
Sebastian Ullrich
989761045b
fix(src/emacs/lean-server): revert 133b70c0 for emacs < 25
2016-10-19 19:47:36 -07:00
Leonardo de Moura
99299d1915
feat(library/tactic/simplify): use propext in rewriting rules when simplify_config.use_axioms is tt
2016-10-19 17:59:01 -07:00
Leonardo de Moura
6edec4c4e9
feat(library/init/meta/converter): implement conversionals using ext_simplify_core
2016-10-19 17:23:32 -07:00
Leonardo de Moura
a4ef8f385d
feat(library/tactic/simplify): add basic support for lambda-expressions
2016-10-19 14:15:56 -07:00
Leonardo de Moura
205d524409
refactor(library/tactic/simplify): delete old simplifier
2016-10-19 14:03:14 -07:00
