Leonardo de Moura
eb8f586dba
fix(library/normalize): fixes #801
2015-08-16 14:22:02 -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
5a6a4b45c1
fix(library/definitional/equations): fixes #796
2015-08-14 14:39:23 -07:00
Leonardo de Moura
d2eb99bf11
refactor(library/logic): move logic/choice.lean to init/classical.lean
...
choice axiom is now in the classical namespace.
2015-08-12 18:37:33 -07:00
Leonardo de Moura
cb9830beaf
refactor(library/logic/choice): move prop_decidable instance into namespace 'classical'
2015-08-12 17:06:15 -07:00
Leonardo de Moura
b4024982a2
refactor(library/data): move vector as indexed family to examples folder
2015-08-12 15:05:14 -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
Jeremy Avigad
305f72bf4f
fix(tests/lean): fix three tests broken by setext renaming
2015-08-09 22:14:25 -04:00
Leonardo de Moura
582dbecfd0
feat(library,hott): add notation T1 : T2 as syntax sugar for (focus (T1; all_goals T2))
...
closes #775
2015-08-08 10:16:25 -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
Floris van Doorn
7f76d7e648
fix(tests): update test
2015-08-07 13:34:41 -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
Floris van Doorn
11b1f416f6
feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries
2015-08-04 13:23:20 +02:00
Floris van Doorn
7a780b1b60
feat(hott): various minor changes in the HoTT library
2015-08-04 13:01:11 +02:00
Leonardo de Moura
0309a1e131
fix(tests/lean/extra/show_goal_bag): adjust test to recent changes in the standard library
2015-08-04 06:52:20 +02: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
656b642c4a
fix(frontends/lean): identifier size when using unicode
...
see issue #756
2015-07-30 11:32:24 -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
d06c2b1ad3
chore(tests/lua/mod5): remove test that regularly timeout on Windows machines
2015-07-29 18:17:06 -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
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
bbd6946a15
refactor(library/logic/axioms): we have only one extra axiom
2015-07-29 13:36:23 -07:00
Leonardo de Moura
6dbcf86fd4
feat(library/logic/axioms): use diaconescu to prove em
...
With the new "noncomputable" feature we can use Hilbert's choice without
being concerned it may accidentaly "leak" inside definitions we don't
want to use it.
2015-07-29 13:01:07 -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
Leonardo de Moura
308af87b69
feat(library): add 'noncomputable' keyword for the standard library
2015-07-28 21:56:35 -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
80e3da0526
fix(library/util): fixes #751
2015-07-28 16:30:20 -07:00
Leonardo de Moura
8ee1d35bed
fix(tests/lean/unfold_crash): fixed regression test for bug reported by Rob
2015-07-28 12:51:42 -07:00
Leonardo de Moura
cfa9412f96
fix(frontends/lean): "show goal" localization, add "position", support "by tactic"
2015-07-28 12:48:12 -07:00
Leonardo de Moura
0dc8dc999e
fix(library/tactic/rewrite_tactic): crash when trying to unfold constructor
2015-07-28 12:43:56 -07:00
Leonardo de Moura
08b23d8b4f
test(tests/lean/extra): add test for "show goal" feature
2015-07-27 21:03:16 -07:00
Leonardo de Moura
a3b570c852
test(tests/lean/extra): test for Soonho
2015-07-27 19:32:27 -07:00
Leonardo de Moura
8c06803f54
test(tests/lean): add regression for issue #737
2015-07-27 07:59:18 -07:00
Leonardo de Moura
f7440ff068
fix(tests/lean): adjust tests to reflect changes in the standard library
2015-07-24 09:59:49 -07:00
Leonardo de Moura
bcf057f4f3
feat(frontends/lean): display '[congr]' attribute when printing theorems
2015-07-23 18:52:59 -07:00
Leonardo de Moura
3e6b80d38c
feat(library/util): disable local constant purification when pretty printing goals
...
This feature generates confusion.
2015-07-23 18:52:59 -07:00
Leonardo de Moura
f1a19a10c4
fix(library/util): incorrect hypothesis renaming when pretty printing goals
2015-07-23 18:52:59 -07:00
