Leonardo de Moura
|
2b52198702
|
fix(library/unfold_macros): fixes #806
|
2015-08-18 17:46:47 -07:00 |
|
Leonardo de Moura
|
3ce8c5d6f7
|
feat(frontends/lean): add "suffices to show A, from B, C" construct
|
2015-08-18 17:04:38 -07:00 |
|
Leonardo de Moura
|
a18983c1aa
|
fix(api/lean_univ): typo
|
2015-08-18 16:01:50 -07:00 |
|
Leonardo de Moura
|
858971c3a5
|
test(tests/shared): add test for the universe C API
|
2015-08-18 15:32:27 -07:00 |
|
Leonardo de Moura
|
d627414f9b
|
feat(api): expose universe expressions in the C API
|
2015-08-18 15:07:44 -07:00 |
|
Leonardo de Moura
|
0909c8f08f
|
chore(CMakeLists): use --export-all in cygwin
|
2015-08-18 13:57:01 -07:00 |
|
Leonardo de Moura
|
53bf7f5ff1
|
fix(src/tests/shared/name): invalid delete
|
2015-08-18 13:56:06 -07:00 |
|
Leonardo de Moura
|
81baa64c77
|
chore(src/api/options): fix style
|
2015-08-18 12:43:58 -07:00 |
|
Leonardo de Moura
|
a1798ed331
|
test(tests/shared): add test for the options C API
|
2015-08-18 12:18:33 -07:00 |
|
Leonardo de Moura
|
da11f7738d
|
feat(api): expose configuration options in the C API
|
2015-08-18 11:57:27 -07:00 |
|
Leonardo de Moura
|
e8e315ff14
|
refactor(api): uniform names
|
2015-08-18 11:01:46 -07:00 |
|
Leonardo de Moura
|
617f55b947
|
chore(src/api): workaround style
|
2015-08-18 10:13:07 -07:00 |
|
Leonardo de Moura
|
52c4133021
|
test(tests/shared/name.c): add anonymous unique test
|
2015-08-18 10:06:50 -07:00 |
|
Leonardo de Moura
|
549eec8a06
|
test(tests/shared/name.c): test exception
|
2015-08-17 18:22:59 -07:00 |
|
Leonardo de Moura
|
9d486a4e88
|
feat(tests/shared): add test for the hierarchical name C API
|
2015-08-17 17:48:09 -07:00 |
|
Leonardo de Moura
|
42d41fb276
|
feat(api): expose hierarchical names in the C API
|
2015-08-17 17:23:10 -07:00 |
|
Leonardo de Moura
|
21c41f50ea
|
fix(frontends/lean/elaborator): fixes #803
|
2015-08-17 14:56:41 -07:00 |
|
Leonardo de Moura
|
4d3ed6ca43
|
feat(init/init): automatically initialize lean shared library
|
2015-08-17 14:18:32 -07:00 |
|
Leonardo de Moura
|
cb7ca51dcb
|
feat(library/unfold_macros): avoid unnecessary get_value
|
2015-08-17 13:03:08 -07:00 |
|
Leonardo de Moura
|
b07a364d2f
|
feat(frontends/lean/parser): process multiple parsing actions
closes #800
|
2015-08-17 09:42:10 -07:00 |
|
Leonardo de Moura
|
d913c04e90
|
feat(frontends/lean/parse_table): add simple notion of "compatible" parsing actions
See issue #800
|
2015-08-17 08:41:30 -07:00 |
|
Leonardo de Moura
|
933850e0d1
|
fix(library/shared_environment): compilation warning
|
2015-08-17 08:41:12 -07:00 |
|
Leonardo de Moura
|
edb4c09bc1
|
fix(frontends/lean,kernel/inductive): compilation errors in Debug mode
|
2015-08-16 19:02:48 -07:00 |
|
Leonardo de Moura
|
ea04414058
|
feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions
see new tests for a summary of new features
see issue #800
|
2015-08-16 18:24:30 -07:00 |
|
Leonardo de Moura
|
ffde40a500
|
fix(frontends/lean/parse_table): missing condition
|
2015-08-16 15:35:17 -07:00 |
|
Leonardo de Moura
|
eb8f586dba
|
fix(library/normalize): fixes #801
|
2015-08-16 14:22:02 -07:00 |
|
Leonardo de Moura
|
1d6bebf3a3
|
feat(frontends/lean/parse_table): start support for multiple "actions" in parsing tables
|
2015-08-16 13:52:06 -07:00 |
|
Leonardo de Moura
|
5f5642c4ce
|
fix(kernel/inductive): compilation error with clang++
|
2015-08-15 15:06:57 -07:00 |
|
Leonardo de Moura
|
7bc8673786
|
feat(library/module): efficient inductive_reader
Do not check imported inductive declarations when trust level is greater than 0.
|
2015-08-15 14:48:49 -07:00 |
|
Leonardo de Moura
|
e80d9685e5
|
refactor(kernel/inductive): add certified_inductive_decl object
We will use this object to implement a more efficient import procedure
|
2015-08-15 13:26:38 -07:00 |
|
Leonardo de Moura
|
b21d85d19e
|
chore(library/coercion): fix style
|
2015-08-14 18:49:01 -07:00 |
|
Daniel Selsam
|
7223293a93
|
feat(library/coercion): improve error message when coercion has no viable source
|
2015-08-14 18:44:44 -07:00 |
|
Daniel Selsam
|
5bef45b1fd
|
feat(library/coercion): improve error message when target is unacceptable
|
2015-08-14 18:44:44 -07:00 |
|
Daniel Selsam
|
f4e1e9d671
|
feat(library/coercion): closes #794
Include level information in primary coercion error message if
pp_options are set to display levels.
|
2015-08-14 18:44:43 -07:00 |
|
Leonardo de Moura
|
6c934229f7
|
feat(kernel,library/module): only module reader can add declarations without type-checking them
|
2015-08-14 18:37:17 -07:00 |
|
Leonardo de Moura
|
11558df6be
|
chore(util/serializer): fix style
|
2015-08-14 18:34:33 -07:00 |
|
Leonardo de Moura
|
d1f13d2871
|
perf(library/module): skip checksum if trust level is very high
|
2015-08-14 18:23:12 -07:00 |
|
Leonardo de Moura
|
d3d1b58fb4
|
perf(util/serializer): minor performance improvement
|
2015-08-14 18:13:08 -07:00 |
|
Leonardo de Moura
|
cc8b5d2d6e
|
perf(library/unfold_macros): skip contains_untrusted_macro if trust level is very high
|
2015-08-14 18:10:19 -07:00 |
|
Leonardo de Moura
|
849b99d244
|
perf(library/module): use block read
|
2015-08-14 17:56:21 -07:00 |
|
Leonardo de Moura
|
54a49bbf2e
|
feat(util/serializer): simple compression trick
reduces the standard library .olean files from 7.2 Mb to 6.1 Mb
|
2015-08-14 15:27:44 -07:00 |
|
Leonardo de Moura
|
5a6a4b45c1
|
fix(library/definitional/equations): fixes #796
|
2015-08-14 14:39:23 -07:00 |
|
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 |
|
Leonardo de Moura
|
a009db2902
|
feat(library): add module for tracking noncomputable definitions
|
2015-07-28 18:15:26 -07:00 |
|
Leonardo de Moura
|
7e8a394caf
|
chore(tests/lean): fix style and adjust tests
|
2015-07-28 18:15:25 -07:00 |
|
Leonardo de Moura
|
b81d4d50f1
|
feat(frontends/lean/bultin_cmds): add 'print axioms <declname>' command that prints axioms a giving declaration depends on
|
2015-07-28 18:15:25 -07:00 |
|
Leonardo de Moura
|
8048cbd6f2
|
feat(kernel): do not hide semi-constructive axioms
|
2015-07-28 18:15:25 -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 |
|
Leonardo de Moura
|
80e3da0526
|
fix(library/util): fixes #751
|
2015-07-28 16:30:20 -07:00 |
|
Leonardo de Moura
|
ad5d792a8e
|
feat(library,shell): add --export-all command line option
|
2015-07-28 15:54:44 -07:00 |
|
Soonho Kong
|
a5da840593
|
fix(emacs/lean-mode.el): typo
|
2015-07-28 14:46:59 -07:00 |
|