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
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
Leonardo de Moura
e221d38790
feat(library/tactic/assert_tactic): allow duplicate names for hypotheses in assert tactic
2015-07-23 18:52:59 -07:00
Leonardo de Moura
e0209a1532
feat(frontends/lean): better error localization for 'have'-expressions in tactic mode
2015-07-23 18:52:59 -07:00
Leonardo de Moura
faab1e449f
fix(tests/lean/rw_set3): update test to reflect changes in the standard library
2015-07-23 18:52:59 -07:00
Leonardo de Moura
5f4576a7f7
test(tests/lean): add test for '[congr]' attribute validation
2015-07-23 18:52:59 -07:00
Leonardo de Moura
844caf32e4
feat(frontends/lean/bultin_cmds): add 'print [congr]' command for displaying active congruence rules
2015-07-23 18:52:59 -07:00
Leonardo de Moura
933f056fff
feat(library/simplifier): add API for extracting simplification rules defined in a given namespace
2015-07-22 18:47:56 -07:00
Leonardo de Moura
8085123119
refactor(library/simplifier): rename 'rewrite_rule' to 'simp_rule'
2015-07-22 10:39:30 -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
23dd47d27f
fix(tests/lean): adjust tests to recent changes to the standard library
2015-07-19 21:32:42 -07:00
Leonardo de Moura
5112232d6d
fix(tests/lean/run/finset): adjust test to recent changes to the
...
standard library
2015-07-19 11:53:21 -07:00
Leonardo de Moura
3ab0e07ba9
feat(frontends/lean): add simp tactic frontend stub
...
This commit also removes the fake_simplifier. It doesn't work anymore
because simp is now a reserved word.
2015-07-14 09:54:53 -04:00
