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

4900 commits

Author SHA1 Message Date
Leonardo de Moura
8c4e5c82ab fix(tests/shared/CMakeFiles): make sure the working directory is the one containing the DLL 2015-08-13 12:31:30 -07:00
Leonardo de Moura
5f8b600024 fix(CMakeLists): use --export-all option when creating DLL on Windows 2015-08-13 12:14:24 -07:00
Leonardo de Moura
3de290db35 fix(tests/shared): include shared_test in the test suite 2015-08-13 11:52:38 -07:00
Leonardo de Moura
52138b8232 fix(CMakeLists): dylib generation 2015-08-13 11:50:41 -07:00
Leonardo de Moura
98bfb8467a test(test/shared): add small program for testing shared library 2015-08-13 11:48:54 -07:00
Leonardo de Moura
8746484b8f fix(CMakeLists): DLL generation 2015-08-13 11:38:33 -07:00
Leonardo de Moura
498afc1e6f feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07:00
Leonardo de Moura
602626803b fix(frontends/lean/builtin_cmds): 'print axioms' and theorem queue 2015-08-11 21:08:45 -07:00
Leonardo de Moura
5d8d226640 fix(frontends/lean/parser): add support for decimals 
Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.

closes #793
 2015-08-11 18:44:48 -07:00
Leonardo de Moura
66a59d5b51 feat(frontends/lean/util): remove hack that overrides priority namespace 
closes #789
 2015-08-11 18:01:40 -07:00
Leonardo de Moura
0b8f57841a feat(frontends/lean/decl_cmds): closes #791 2015-08-11 17:53:33 -07:00
Soonho Kong
6443de67d4 feat(emacs/lean-mode): lean-exec-at-pos uses timer to wait until flycheck process is over 
close #790
 2015-08-11 20:17:53 -04:00
Daniel Selsam
40471ca8e3 doc(frontends/lean/elaborator): assert invariant in visit_app 2015-08-11 17:02:38 -07:00
Leonardo de Moura
23118371d1 refactor(library/aliases): cleanup 2015-08-11 06:41:56 -07:00
Soonho Kong
00582934ec feat(CMakeLists.txt): update CXX_FLAGS_EMSCRIPTEN 
Add: -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1

Close leanprover/tutorial#96
 2015-08-10 02:03:39 -04:00
Soonho Kong
938dae7b19 refactor(emacs/lean-syntax.el): clean up regexps for syntax 2015-08-08 09:55:16 -07:00
Leonardo de Moura
1f34c72192 fix(frontends/lean/parser): fixes #770 2015-08-08 09:48:31 -07:00
Leonardo de Moura
dc2e702373 feat(library/unifier): generate approximate solution for universe constraints of the form (max u ?m =?= max u v) 
closes #777
 2015-08-08 09:29:59 -07:00
Leonardo de Moura
6c5832a564 feat(frontends/lean/decl_cmds): allow recursive examples 
closes #774
 2015-08-08 08:26:25 -07:00
Leonardo de Moura
06f20694c8 fix(frontends/lean/builtin_exprs): fixes #768 2015-08-08 04:20:17 -07:00
Leonardo de Moura
d46dbce86e feat(library/tactic/tactic): apply substitution in 'then' combinator 
closes #778
 2015-08-08 03:42:21 -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
Leonardo de Moura
5568085ab9 fix(frontends/lean/elaborator): closes #771 
Produce nicer error message when type/goal is a metavariable and
universe metavariables have already been instantiated with universe
parameters.
 2015-08-07 13:29:22 -07:00
Leonardo de Moura
6a079fdd2d fix(library/tactic/exact_tactic): fixes #779 2015-08-07 13:29:22 -07:00
Leonardo de Moura
f21647899f feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this' 
This is useful if 'show' is recursive
 2015-08-07 13:29:21 -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
Leonardo de Moura
60ba3d15ff feat(library/data/matrix): add basic matrix module 2015-08-01 19:33:31 +01:00
Leonardo de Moura
1f304ad4b9 fix(frontends/lean/pp): pretty printing 'binder' 
This commit also replaces many occurrences of 'binders' with 'binder'.
 2015-07-31 11:27:38 -07:00
Leonardo de Moura
8f5a760b89 feat(frontends/lean/elaborator): display the whole proof state in option "--goal" 
see issue #755
 2015-07-31 08:56:17 -07:00
Leonardo de Moura
f264adfa92 fix(library/export): bug in --export-all option 2015-07-30 17:23:38 -07:00
Leonardo de Moura
9bf64c10fd feat(library/export): export the whole environment when using "--expor-all" 2015-07-30 15:04:49 -07:00
Soonho Kong
bed751a2d7 feat(emacs/lean-settings.el): add lean-keybinding customize group 
close #758
 2015-07-30 11:33:17 -07:00
Leonardo de Moura
656b642c4a fix(frontends/lean): identifier size when using unicode 
see issue #756
 2015-07-30 11:32:24 -07:00
Leonardo de Moura
a39cac4fad feat(frontends/lean): improve '--info' command line option 
see issue #756
 2015-07-30 11:05:39 -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
cc4f18c062 feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information 
see issue #756
 2015-07-30 10:18:03 -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
Leonardo de Moura
384ccf2b6c feat(frontends/lean/elaborator): change behavior of "show goal" for incomplete "by tactic" 
If "by tactic" did not completely solved the goal, then we show the
final state when the user presses "C-c C-g"
 2015-07-29 17:34:42 -07:00
Leonardo de Moura
b3707ab54a feat(library/tactic/unfold_rec): fixes #753 2015-07-29 17:13:02 -07:00
Leonardo de Moura
ed41a01a51 fix(frontends/lean/elaborator): fixes #755 2015-07-29 16:41:30 -07:00
Leonardo de Moura
0bda39c8ac feat(frontends/lean): check for noncomputability when moving theorems from theorem_queue to environment 2015-07-29 13:01:07 -07:00
Leonardo de Moura
69ead0ddd8 feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations 2015-07-29 13:01:07 -07:00
Leonardo de Moura
74be3031b1 feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions 2015-07-29 13:01:06 -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