Soonho Kong
|
60d14b50ab
|
feat(emacs/lean-require): check lean-mode dependencies in initialization
Close #91
|
2014-09-09 15:11:57 -07:00 |
|
Soonho Kong
|
961dccf279
|
feat(emacs/Cask): add Cask file
Close #92
|
2014-09-09 15:11:57 -07:00 |
|
Leonardo de Moura
|
47e02342bb
|
feat(frontends/lean/elaborator): use whnf in class-instance resolution, closes #160
|
2014-09-09 15:04:44 -07:00 |
|
Leonardo de Moura
|
bd1bc336fb
|
feat(library/coercion): add simple trick for defining coercions to function-class in a convenient way, closes #31
|
2014-09-09 14:36:36 -07:00 |
|
Leonardo de Moura
|
abdd784729
|
feat(shell): start 'lean --server' with 'pp.beta = true'
|
2014-09-09 14:13:35 -07:00 |
|
Leonardo de Moura
|
2d94584816
|
feat(frontends/lean/pp): add 'pp.beta' option, closes #154
|
2014-09-09 14:10:20 -07:00 |
|
Leonardo de Moura
|
65000fa653
|
feat(library/coercion): rename class to 'coercions'
|
2014-09-09 14:03:45 -07:00 |
|
Leonardo de Moura
|
38a4852e7d
|
feat(library/hott): add 'path' namespace
|
2014-09-09 14:03:45 -07:00 |
|
Leonardo de Moura
|
ff9a07500d
|
feat(library/data/int/basic): create alias for int.int
|
2014-09-09 14:03:44 -07:00 |
|
Soonho Kong
|
ba6dc59d5f
|
fix(emacs/lean-server): missing 'rx' at the beginning of regex
|
2014-09-09 13:47:09 -07:00 |
|
Soonho Kong
|
70dcc2e122
|
fix(emacs): use looking-at instead of char-after
|
2014-09-09 13:22:58 -07:00 |
|
Soonho Kong
|
85bd112a37
|
fix(emacs/lean-company): color problem when showing auto-complete candidates
|
2014-09-09 13:22:58 -07:00 |
|
Soonho Kong
|
c26f39b86e
|
feat(emacs/lean-company): "c-u TAB" asks filter for FINDG
|
2014-09-09 13:22:58 -07:00 |
|
Leonardo de Moura
|
ee196bbf1a
|
fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151
|
2014-09-09 12:49:32 -07:00 |
|
Leonardo de Moura
|
d8caa294b5
|
fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-09 11:02:54 -07:00 |
|
Soonho Kong
|
c5d20aaa9d
|
fix(bin/linja): pass args to call_lean and handle_failure_for_flycheck
Fix #163
|
2014-09-09 10:52:32 -07:00 |
|
Soonho Kong
|
3950e341e0
|
fix(bin/linja): allow non-exist cache argument
Fix #163
|
2014-09-09 10:45:56 -07:00 |
|
Leonardo de Moura
|
0505be2aca
|
feat(frontends/lean/server): unifier maximum number of steps error in FINDG, closes #155
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-09 10:36:41 -07:00 |
|
Leonardo de Moura
|
53292d8297
|
feat(frontends/lean/server): add timebound to WAIT command, closes #156
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-09 10:28:47 -07:00 |
|
Soonho Kong
|
dab9ef31e3
|
feat(bin/linja): add build_ninja_and_save_at
Fix #129
|
2014-09-09 09:50:06 -07:00 |
|
Leonardo de Moura
|
05c6e1461e
|
fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-09 09:47:19 -07:00 |
|
Leonardo de Moura
|
187661aa6a
|
feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
a5698a55ec
|
fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
fd85d4702e
|
refactor(library/unifier): move all_local outside of the class
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
ebde1bcfad
|
feat(library/unifier): option 'unifier.computation true' will force elaborator to always consider an extra case-split when the right-hand-side of a flex-rigid constraint is not in weak-head-normal-form
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
d9afb3ca96
|
fix(frontends/lean/elaborator): missing constraint
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
5087f03889
|
refactor(library/logic/classes/decidable): rename 'decidable_eq_to_decidable' theorem to 'of_decidable_eq'
|
2014-09-09 09:27:26 -07:00 |
|
Leonardo de Moura
|
4088cdc139
|
chore(frontend/lean/pp_options): use consistent name convention for pp option names
|
2014-09-09 09:27:26 -07:00 |
|
Soonho Kong
|
b460c02017
|
feat(emacs/lean-mode): add imenu support
Close #97
|
2014-09-09 09:04:31 -07:00 |
|
Soonho Kong
|
4eb8a9b192
|
feat(emacs/lean-flycheck): "real" .clean file instead of "flycheck_real.clean"
Fix #140
|
2014-09-08 23:49:02 -07:00 |
|
Soonho Kong
|
f39e21f90e
|
feat(bin/linja): add --cache option
Needed to solve #140
|
2014-09-08 23:49:02 -07:00 |
|
Soonho Kong
|
18bcfc535a
|
feat(bin/linja): add --flycheck-max-messages
Close #134
|
2014-09-08 18:44:22 -07:00 |
|
Soonho Kong
|
a9be084b1c
|
feat(emacs/lean-settings): add lean-flycheck-pp-width and lean-flycheck-max-messages-to-display
|
2014-09-08 18:44:22 -07:00 |
|
Soonho Kong
|
3682ca32d2
|
feat(emacs/lean-company): call FINDG if cursor is at "_"
|
2014-09-08 16:04:20 -07:00 |
|
Soonho Kong
|
4f604544c4
|
feat(emacs/lean-cmd): add WAIT command
|
2014-09-08 16:04:19 -07:00 |
|
Soonho Kong
|
c88bfc0c02
|
chore(frontends/lean/server.cpp): add BEGIN/END for WAIT command
|
2014-09-08 16:04:19 -07:00 |
|
Soonho Kong
|
bc640510aa
|
feat(emacs/lean-cmd): add FINDG cmd
|
2014-09-08 16:04:19 -07:00 |
|
Soonho Kong
|
0ac1ec1de3
|
feat(emacs/lean-settings): add lean-show-only-type-in-parens
Fix #135
|
2014-09-08 11:39:40 -07:00 |
|
Soonho Kong
|
a40894a712
|
fix(emacs/lean-tags): pass lean-flycheck-checker-options properly
Fix #153
|
2014-09-08 11:27:04 -07:00 |
|
Soonho Kong
|
c365f6b9ab
|
fix(emacs/lean-company): only activate auto-completion when TAB is pressed
|
2014-09-08 10:52:22 -07:00 |
|
Soonho Kong
|
6c483467dd
|
feat(emacs/lean-company): replace ?M in AC candidate with M and colorize
close #149
|
2014-09-08 09:47:51 -07:00 |
|
Leonardo de Moura
|
11addbb594
|
fix(frontend/lean/server): auto completion doesn't use prefix, fixes #147
|
2014-09-08 08:04:04 -07:00 |
|
Leonardo de Moura
|
b4793df653
|
feat(frontends/lean): rename '[fact]' to '[visible]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-08 07:47:42 -07:00 |
|
Leonardo de Moura
|
35e68fea76
|
feat(library/logic/classes/decidable): generalize 'by_cases' theorem
|
2014-09-08 00:16:20 -07:00 |
|
Leonardo de Moura
|
fa25ddc8e6
|
chore(library/data/int/basic): remove unnecessary 'hinding' clause
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-07 22:50:43 -07:00 |
|
Leonardo de Moura
|
559dd586f2
|
feat(library): add 'decidable_eq' class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-07 22:23:36 -07:00 |
|
Leonardo de Moura
|
c446327ec3
|
feat(library/data/list): add mem_is_decidable and not_mem_find theorems
|
2014-09-07 21:22:07 -07:00 |
|
Leonardo de Moura
|
cbdfb0dcdc
|
feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77
|
2014-09-07 19:59:34 -07:00 |
|
Leonardo de Moura
|
2631979f5c
|
fix(library/scoped_ext): section/context should not affect namespace
|
2014-09-07 19:59:34 -07:00 |
|
Leonardo de Moura
|
f9b62c53e6
|
feat(library/data/nat): add nat.is_inhabited theorem
|
2014-09-07 19:59:34 -07:00 |
|