Jeremy Avigad
bcad5309d9
fix(library/init/meta/interactive): implement docstring fixes from kha
2017-09-22 16:53:22 -04:00
Jeremy Avigad
57f9cbeb78
fix(tests/lean/interactive/*): fix tests
2017-09-21 21:16:20 -04:00
Jeremy Avigad
41b94ed3a2
refactor/feat(library/init/meta/interactive): revise and add docstrings
2017-09-21 21:15:41 -04:00
Mario Carneiro
d83b9ef3ef
fix(init/algebra/ordered_ring): theorem has two instances
2017-09-18 13:04:59 -07:00
Sebastian Ullrich
d54c4e11c2
feat(emacs): highlight flycheck and eldoc output
2017-09-18 13:02:06 -07:00
Leonardo de Moura
f0bf1624fe
feat(frontends/lean/brackets): closes #1820
2017-09-15 12:54:21 -07:00
Sebastian Ullrich
650b4ab3dc
chore(.travis.yml): undo Travis update
...
The test_registry test is failing because `python3` seems to have reverted to Python 3.4 in a Travis upgrade. Probably related to https://github.com/travis-ci/travis-ci/issues/8315#issuecomment-327537437 .
2017-09-15 12:33:46 -07:00
Mario Carneiro
983328806b
chore(init/algebra/group): generalize to noncomm groups
2017-09-15 12:33:46 -07:00
Mario Carneiro
9e34ee94eb
chore(init/algebra/ordered_ring): generalize thm to noncommutative rings
2017-09-15 12:33:46 -07:00
Mario Carneiro
5c8409b1a0
chore(init/data/nat/lemmas): pred_le_pred: remove superfluous assumption
2017-09-15 12:33:46 -07:00
Leonardo de Moura
f36fca875c
feag(frontends/lean): explicit delimiters in declaration parameters
...
Comment from parser.h
This commit makes sure that all declaration parameters must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
The goal is to avoid counter-intuitive declarations such as:
example p : false := trivial
def main proof : false := trivial
which would be parsed as
example (p : false) : _ := trivial
def main (proof : false) : _ := trivial
where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.
Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to write
fun x : t, s
or
fun x, s
instead of
fun (x : t), s
2017-09-15 10:07:09 -07:00
Gabriel Ebner
3d711b37c3
chore(*): development version 3.3.1
2017-09-14 18:55:03 +02:00
Gabriel Ebner
fa9c868ed2
chore(*): version 3.3.0
2017-09-14 18:53:38 +02:00
Sebastian Ullrich
7ff06b2184
chore(init/meta/attribute): rename user_attribute.set_param to user_attribute.set
...
Setting the parameter value really is a side effect of setting the whole attribute
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
928e982565
chore(init/meta/mk_has_reflect_instance): disallow indexed families for now
...
We need to adapt the recursion code to pass `reflected` instances for indices
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
6549643d39
chore(init/meta/derive): remove inhabited derive handler for now
...
The generated instances were unnecessarily restrictive
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
8d9c0ac806
fix(frontends/lean/tactic_notation): by tactic: accept non-atomic proof
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
3c68f6fa00
fix(leanpkg): fix error message
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
87b39bd1c3
fix(init/meta/derive): handle indexed families
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
2faad5114a
chore(frontends/lean): enforce and document applying attributes last
2017-09-14 18:48:18 +02:00
Sebastian Ullrich
aa3c707ab4
chore(init/meta/derive): document
2017-09-14 18:48:18 +02:00
Gabriel Ebner
341cf71fb9
fix(frontends/lean/structure_cmd): check parent expression after elaboration as well
2017-09-14 09:36:40 +02:00
Leonardo de Moura
6781681ae5
feat(frontends/lean/definition_cmds): when the kernel fails to type check a declaration include the fully elaborated term in the error message
2017-09-13 16:43:54 -07:00
Leonardo de Moura
dbe1033427
fix(library/init/meta/mk_has_sizeof_instance): indexed families
...
see #1818
2017-09-12 15:17:34 -07:00
Gabriel Ebner
9118079f7f
fix(library/module_mgr): error handling in cyclic imports
...
Fixes #1807
2017-09-12 17:22:47 +02:00
Sebastian Ullrich
5410178203
chore(init/meta/mk_has_reflect_instance): document
2017-09-11 16:56:03 -07:00
Sebastian Ullrich
4d1c4aee03
feat(init/meta/mk_has_reflect_instance): add derive_handler for has_reflect
2017-09-11 16:56:03 -07:00
Sebastian Ullrich
e18a14d6e0
fix(init/meta/expr): reflected.subst should always return an expr of the correct type
2017-09-11 16:56:03 -07:00
Sebastian Ullrich
f2c5342aaa
feat(init/meta/derive): handle parameters, parameter instances, universes
2017-09-11 16:56:03 -07:00
Sebastian Ullrich
7412512579
fix(frontends/lean/structure_cmd): apply attributes last
2017-09-11 16:56:02 -07:00
Sebastian Ullrich
230bf7e8d9
fix(frontends/lean/decl_cmds): constant/axiom cmds: apply attributes
2017-09-11 16:56:02 -07:00
Leonardo de Moura
d428eca8a7
fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations
...
fixes #1804
Remark: now, all auxiliary definitions in a private declaration share
the same "private" prefix.
2017-09-11 16:46:56 -07:00
Sebastian Ullrich
d82df26ff0
fix(frontends/lean/elaborator): go back to ignoring implicit args in quote patterns
2017-09-11 09:33:38 -07:00
Sebastian Ullrich
f242d04d55
chore(emacs/lean-dev): lean-diff-test-file produced wrong paths
2017-09-10 09:53:23 +02:00
Sebastian Ullrich
869ac974b2
fix(init/meta/interactive): assume: use rbp 2
2017-09-10 09:53:07 +02:00
Sebastian Ullrich
0bf96e5752
fix(frontends/lean/elaborator): revert dubious workaround of mine
...
Synthesizing an expr placeholder in an elaborated term doesn't make much sense
2017-09-08 13:23:16 +02:00
Leonardo de Moura
1f757ba84e
fix(frontends/lean/pp): fixes #1817
2017-09-07 15:23:58 -07:00
Mario Carneiro
87f2ec08ad
feat(init/meta/interactive): suffices tactic
...
Just a simple manipulation of the `have` tactic, but it allows the use of `suffices h : T, from p,` in tactic mode.
2017-09-06 10:50:31 -07:00
Gabriel Ebner
19777cf9eb
fix(frontends/lean/definition_cmds): show trace messages in examples
2017-09-06 14:44:44 +02:00
Gabriel Ebner
5adb3630b2
chore(tests): update test output
2017-09-06 14:27:39 +02:00
Gabriel Ebner
5f8cf45073
feat(frontends/lean/elaborator): apply to-sort coercion also in arguments
2017-09-06 14:15:30 +02:00
Gabriel Ebner
7b18d5828d
feat(frontends/lean/elaborator): trigger coe_to_fun even when expected type has metavariables
...
We only need to know that the expected type is a Π to perform
to-function coercion. Related to #1402 .
Fixes https://github.com/gebner/hott3/issues/2
2017-09-06 11:20:04 +02:00
Gabriel Ebner
b59d2771ea
fix(doc/changes): describe fallout from parameterized user attributes
...
@kha This was an unexpected breakage resulting from #1809 .
2017-09-06 08:39:30 +02:00
Leonardo de Moura
88cd294a09
feat(src/kernel/error_msgs): show aliased variables when printing error messages
...
closes #1814
@kenmcmil: the error messages will now list aliased variables.
For example, in your file, the new error message is:
```
invalid type ascription, term has type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
but is expected to have type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
types contain aliased name(s): c'
remark: the tactic `dedup` can be used to rename aliases
state:
...
```
2017-09-05 16:46:44 -07:00
Leonardo de Moura
51bac2918f
chore(library/init/core): declare and using structure
...
This change was requested by several users.
2017-09-05 15:08:20 -07:00
Leonardo de Moura
3af8ca11bc
chore(tests/lean/run/1797): add test for #1797
2017-09-05 14:36:51 -07:00
Mario Carneiro
cc9de4af58
feat(init/meta/interactive): cases with equality
...
This is the equivalent of the `ginduction` tactic for cases, but rolled into the same syntax as `cases` itself. `cases h : term` is the syntax, and it will introduce a hypothesis `h : term = C a b...` demonstrating that the original term is equal to the current case.
I considered the possibility of calling `injection` on the generated equalities, but it's useless in the casaes when the equality carries some real information (such as `f x = C1 a`), and when the input term is a local constant, `injection` will do subst, which will undo the effect of the `cases`. If the input term is a constructor, then `injection` would do something interesting, but you would never want to call `cases` in this case because the constructor is already exposed.
2017-09-05 14:31:52 -07:00
Leonardo de Moura
8a10d4c72c
fix(library/init/meta/injection_tactic): fixes #1805
2017-09-05 14:20:22 -07:00
Sebastian Ullrich
0dc9d1b4ac
chore(doc/changes): update changelog
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
1544c3d390
feat(library/tactic/user_attribute,init/meta/attribute): user_attribute.set_param
2017-09-05 23:14:34 +02:00
