michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
6955 commits 3 branches 0 tags 28 MiB
Commit graph

499 commits

Author SHA1 Message Date
Soonho Kong
938dae7b19 refactor(emacs/lean-syntax.el): clean up regexps for syntax 2015-08-08 09:55:16 -07:00
Jeremy Avigad
d6bde18b46 feat,refactor(library/data/{finset,set}/*,src/emacs/lean-input.el): add powerset and notation, and some tidying 2015-08-07 13:45:15 -07:00
Soonho Kong
f9b069b6a5 fix(emacs/lean-company.el): set timeout for company-lean--import-candidates 
Custom variable lean-company-import-timeout is added (default: 1sec).

Close #766
 2015-08-06 22:53:49 -04:00
Soonho Kong
a4014fb532 feat(emacs/lean-util.el): add lean-find-files 2015-08-06 22:48:00 -04:00
Soonho Kong
7d1895928a fix(emacs/lean-mode.el): use original extension when make temp-file 
close #767
 2015-08-05 12:51:09 -04:00
Soonho Kong
795728267d doc(emacs/README.md): update MELPA instruction 2015-08-03 09:27:16 -04:00
Soonho Kong
bed751a2d7 feat(emacs/lean-settings.el): add lean-keybinding customize group 
close #758
 2015-07-30 11:33:17 -07:00
Soonho Kong
c390550340 feat(emacs/lean-mode.el): add show-goal-at-pos and show-id-keyword-info in the menu 2015-07-30 10:46:47 -07:00
Soonho Kong
46a79ec43d feat(emacs/lean-mode.el): add lean-show-id-keyword-info 
close #756
 2015-07-30 10:46:10 -07:00
Leonardo de Moura
be61fb0566 feat(frontends/lean/elaborator): add "noncomputable theory" command, display "noncomputable" when printing definitions 
When the command "noncomputable theory" is used, Lean will not sign an
error when a noncomputable definition is not marked as noncomputable
 2015-07-29 17:54:35 -07:00
Soonho Kong
8a9f774611 fix(emacs/lean-mode.el): lean-exec-at-pos don't ask to save 
close #752
 2015-07-29 10:28:18 -07:00
Soonho Kong
5d159ea664 fix(emacs/lean-mode.el): fix wrong parens in lean-show-goal-at-pos 2015-07-28 22:11:35 -07:00
Leonardo de Moura
308af87b69 feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -07:00
Soonho Kong
1829e64a76 feat(emacs/lean-server.el): lean-server-consume-all-async-tasks restart lean-server if necessary 
related issue: #263
 2015-07-28 18:14:16 -07:00
Soonho Kong
a5da840593 fix(emacs/lean-mode.el): typo 2015-07-28 14:46:59 -07:00
Soonho Kong
0fed6129df feat(emacs/lean-mode): add lean-show-goal-at-pos 
which is bound to 'C-c C-g' by default. Depending on the current char,
it invokes lean-server with either '--goal' or '--hole' option.

close #749
 2015-07-28 14:17:36 -07:00
Soonho Kong
f71987612f fix(emacs/lean-syntax.el): update lean-info syntax highlight 
close #748
 2015-07-28 11:51:01 -07:00
Soonho Kong
72f0fc29fd fix(emacs/lean-mode.el): check header and footer in lean-exec-at-pos-extract-body 
close #747
 2015-07-28 11:13:31 -07:00
Soonho Kong
e61a61da8b feat(emacs/lean-mode.el): use lean-info-mode in lean-exec-at-pos 2015-07-27 20:26:28 -07:00
Soonho Kong
a9630edfed feat(emacs/lean-mode.el): handle delimiter for lean-exec-at-pos 
Related issue: #499
 2015-07-27 19:28:16 -07:00
Leonardo de Moura
3fb16d6287 feat(frontends/lean): add "show hole" command line option 2015-07-27 18:42:57 -07:00
Leonardo de Moura
68370d5c8e feat(frontends/lean): process "show goal" command line option 2015-07-27 17:44:43 -07:00
Soonho Kong
6de86ff749 fix(emacs/lean-mode.el): attach sentinel to lean-exec-at-pos 
Close #499

Usage:

(add-hook 'lean-mode-hook '(lambda ()
(lean-define-key-binding "\C-c\C-g"
                     '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))
 2015-07-27 13:17:16 -07:00
Leonardo de Moura
18dd7c13f9 feat(frontends/lean): add '[congr]' attribute 2015-07-22 17:21:47 -07:00
Leonardo de Moura
092c8d05b9 feat(frontends/lean,library): rename '[rewrite]' to '[simp]' 2015-07-22 09:01:42 -07:00
Leonardo de Moura
812ddf1ef5 feat(frontends/lean): add 'suppose'-expression 
It is a variant of 'assume' that allow anonymous declarations.
 2015-07-19 12:15:12 -07:00
Leonardo de Moura
92f8eb173b feat(frontends/lean): use 'this' as the name for anonymous 'have'-expression 2015-07-18 13:36:05 -05:00
Soonho Kong
014a5ea83e fix(emacs/load-lean.el): add let-alist 
close #729
 2015-07-15 16:07:35 -07:00
Leonardo de Moura
267545ca0c feat(frontends/lean): parse 'with_options' tactical 
see issue #492
 2015-07-13 19:13:41 -04:00
Leonardo de Moura
4b1b3e277f feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]' 
see issue #693
 2015-07-07 16:37:06 -07:00
Leonardo de Moura
3215af3926 feat(frontends/lean): add '[trans-instance]' attribute 
see issue #666
 2015-06-27 14:07:29 -07:00
Floris van Doorn
c8eee66c5b feat(hott/relation): add equivalence closure of a relation 2015-06-25 22:31:41 -04:00
Floris van Doorn
ea0f57aef5 feat(hott): various clean-up and small additions 2015-06-25 22:31:40 -04:00
Leonardo de Moura
a4c0699e81 feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic 
See issue #676

Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
 2015-06-17 23:48:54 -07:00
Leonardo de Moura
3d9b557cfd feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions 
closes #484
 2015-06-12 17:49:26 -07:00
Floris van Doorn
ff41886a32 feat(nat/bquant): give instances for quantification bounded with le 
also add theorems c_iff_c to logic/connectives, where c is a connective
 2015-06-04 20:14:13 -04:00
Leonardo de Moura
cfb102cbd1 fix(emacs/lean-mode): disable electric-indent-mode 
closes #636
 2015-06-01 22:42:57 -07:00
Leonardo de Moura
0fbc944cdd feat(frontends/lean): add '[rewrite]' attribute 2015-06-01 17:58:24 -07:00
Leonardo de Moura
85409a59d3 feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants 
closes #511
 2015-05-27 16:32:43 -07:00
Floris van Doorn
c64d73aae4 feat(types.nat): prove that inequalities on nat are mere propositions 
Also some small changes in various other locations
 2015-05-26 21:37:01 -07:00
Floris van Doorn
8396c4c824 feat(lean-syntax): color abbreviations yellow 2015-05-26 21:37:01 -07:00
Soonho Kong
c4ec89ae6d fix(emacs/lean-flycheck.el): use -concat in lean-flycheck-command 2015-05-26 17:00:05 -04:00
Soonho Kong
1d25f9fa06 fix(emacs/lean-util.el): use f-join instead of lean-concat-paths 2015-05-26 17:00:05 -04:00
Soonho Kong
ce10d5ca08 fix(emacs/lean-flycheck.el): use flycheck-increment-error-columns instead of advice 
Comment from @lunaryorn (flycheck author):

"Please don't use an advice to increment error columns. Flycheck has
:error-filters and there is even a built-in one exactly for your use
case: :error-filter flycheck-increment-error-columsn. Generally never
use advises at all in libraries or modes. They are for user
configuration, or as a very last resort only."
 2015-05-26 17:00:05 -04:00
Soonho Kong
ac04b996ab fix(emacs/lean-flycheck.el): use flycheck-define-command-checker 
Comment from @lunaryorn (flycheck author):

"eval around flycheck-define-checker breaks byte compilation and
scoping. Please use flycheck-define-command-checker if you need to
create :command dynamically."
 2015-05-26 17:00:05 -04:00
Leonardo de Moura
d0987eb3ac feat(library/tactic): add 'subtvars' tactic 2015-05-25 16:36:44 -07:00
Leonardo de Moura
af3f0088f4 feat(frontends/lean): add 'override' (notation) command 2015-05-20 11:42:16 -07:00
Leonardo de Moura
90ea4995f4 fix(emacs/lean-syntax): remove deprecated keywords 2015-05-19 18:34:14 -07:00
Floris van Doorn
2144036cdb feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups 
Also many minor fixes at various places
 2015-05-18 15:59:55 -07:00
Leonardo de Moura
c61c049152 feat(library/user_recursors): generalize acceptable use-defined recursors 
see issue #492
 2015-05-18 14:21:10 -07:00