Leonardo de Moura
40fc64480a
feat: add tactic subst_vars
2022-05-28 16:19:34 -07:00
Leonardo de Moura
2c5bafcbd8
fix: dead variables at match equation hypotheses
...
This commit addresses an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structural.20Recursion.20Problem/near/284238723
2022-05-28 16:09:35 -07:00
Leonardo de Moura
e26f86dd45
fix: improve simpH?, remove unnecessary hypotheses
2022-05-28 15:30:01 -07:00
Leonardo de Moura
34bbe5d12c
feat: add simp theorem List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
2022-05-27 18:26:48 -07:00
Leonardo de Moura
fbd8224b4d
fix: allow recursive occurrences in binder types at WF/PackDomain.lean
...
fixes #1171
2022-05-27 11:23:51 -07:00
Leonardo de Moura
3be437cad3
fix: make sure register_simp_attr declares an simp-like attribute parser for user simp attributes
...
closes #1164
2022-05-26 19:49:33 -07:00
Leonardo de Moura
7d8f8c0fbe
chore: style
2022-05-26 15:18:07 -07:00
Leonardo de Moura
25126cd057
fix: autoParam is structure fields lost in multiple inheritance
...
closes #1158
2022-05-26 14:35:47 -07:00
Leonardo de Moura
b4c1163f8f
chore: update stage0
2022-05-26 14:22:38 -07:00
Leonardo de Moura
f48b822532
feat: add field for storing autoParam information at StructureFieldInfo
...
We need this information when copying fields from parent structures.
We don't use hacks such as traversing the parent constructor type.
2022-05-26 14:21:03 -07:00
Leonardo de Moura
dcb974a1cf
chore: remove unused parameter
2022-05-26 14:20:51 -07:00
Leonardo de Moura
fc606f3ab5
fix: closes #1156
2022-05-26 12:51:28 -07:00
Leonardo de Moura
988697b431
fix: fixes #1169
2022-05-26 07:05:32 -07:00
Leonardo de Moura
1d14637680
fix: missing withMVarContext
2022-05-26 06:18:14 -07:00
Leonardo de Moura
fad21a4cda
chore: remove leftovers
2022-05-25 20:38:20 -07:00
Leonardo de Moura
944063682e
fix: another specialize.cpp bug
...
This is just a workaround. This code has to be ported to Lean.
The issue has been reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20unknown.20constant/near/283750650
2022-05-25 20:36:18 -07:00
Leonardo de Moura
dca8a8ed98
fix: match or-pattern
...
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Probably.20a.20bug/near/283779934
2022-05-25 20:05:46 -07:00
Leonardo de Moura
bef1cd4872
fix: make structure instance notation (e.g., { a, b }) works in patterns after we define the Set notation in Mathlib
2022-05-25 19:14:22 -07:00
Leonardo de Moura
a26827f58b
chore: remove Context.main
2022-05-25 11:58:33 -07:00
Jannis Limperg
6dc5ddac35
fix: apply after-compilation attributes to inductive/structure decls
...
Attributes with `AttributeApplicationTime.afterCompilation` were
silently not applied to `inductive` and `structure` declarations.
2022-05-25 11:32:08 -07:00
Sebastian Ullrich
4a1885f997
chore: update benchmark suite
2022-05-25 18:26:36 +02:00
asdasd1dsadsa
794877c0c8
chore: add option to exclude 'LICENSE' files from 'make install'
2022-05-25 12:39:30 +02:00
Sebastian Ullrich
b97fb23dbe
chore: update stage0
2022-05-25 09:48:11 +02:00
Sebastian Ullrich
0a39e9cbdc
fix: dynamic quotations should use previous stage by default
...
@leodemoura as discussed some time ago
2022-05-25 09:46:10 +02:00
Leonardo de Moura
cb32681978
doc: add slide headers to examples
2022-05-23 18:20:37 -07:00
Leonardo de Moura
bf5f107e74
doc: missing NFM examples
2022-05-23 18:04:03 -07:00
Leonardo de Moura
7c427c1ef2
fix: make sure let-expressions do not affect the structural recursion module
...
This issue has been reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Termination.20check.20not.20preserved.20under.20let.20binding.2E/near/282934378
2022-05-23 13:42:48 -07:00
Leonardo de Moura
655c9fafa4
chore: update stage0
2022-05-23 12:00:10 -07:00
Leonardo de Moura
d05dff078a
chore: update stage0
2022-05-23 11:56:59 -07:00
Leonardo de Moura
2fc23a2a2b
feat: make sure we can use split to synthesize code
2022-05-23 11:55:57 -07:00
Leonardo de Moura
e552558f2f
chore: style
2022-05-23 11:04:29 -07:00
Leonardo de Moura
6ce6b12707
doc: NFM'22 examples
2022-05-22 19:21:30 -07:00
Leonardo de Moura
56cd6c1ff5
fix: we should not use implicit targets when creating the key for the CustomEliminator map
2022-05-20 06:55:23 -07:00
Leonardo de Moura
063c77037f
chore: fix typo
2022-05-20 06:44:25 -07:00
E.W.Ayers
8ef0154403
refactor: rpc -> serverRpcMethod
2022-05-19 18:53:19 +02:00
E.W.Ayers
3bdb98e5ee
feat: rpc attribute
...
Functions can now be marked with the `@[rpc]` attribute, which
registers the function as an RpcProcedure that can be used to
communicate with the code editor and infoview.
2022-05-19 18:53:19 +02:00
Sebastian Ullrich
d13fac6f45
doc: update quickstart
2022-05-18 17:43:14 +02:00
Sebastian Ullrich
c3a9831388
doc: document ‹t›
2022-05-18 10:32:06 +02:00
Sebastian Ullrich
1d44c30b3f
refactor: simplify log2 termination proof
2022-05-18 10:20:36 +02:00
Sebastian Ullrich
eb170d1f43
fix: compiled string literals containing null bytes
2022-05-17 09:24:34 -07:00
Sebastian Ullrich
1e271c3432
chore: CI: document ridiculous workaround
2022-05-17 17:45:58 +02:00
Sebastian Ullrich
14225b81ce
chore: CI: really?
2022-05-17 15:53:33 +02:00
Sebastian Ullrich
a2bf2a4abd
fix: info at pattern variables
2022-05-17 06:28:59 -07:00
Sebastian Ullrich
61c7b8b94c
chore: format string
2022-05-16 15:14:01 +02:00
Sebastian Ullrich
46df02877d
fix: elab info for decreasing_by
2022-05-16 10:20:49 +02:00
Sebastian Ullrich
bfb9dc0697
chore: CI: really do not build nightlies on forks
2022-05-16 09:58:26 +02:00
Sebastian Ullrich
4934104eaf
chore: update script/reformat.lean
2022-05-13 11:55:44 +02:00
Wojciech Nawrocki
5cd4bd3552
refactor: auto-derive RpcEncoding
2022-05-12 13:22:37 -07:00
Wojciech Nawrocki
a8cfbb11bf
Revert "chore: fix tests"
...
This reverts commit c6acd968d7
2022-05-12 13:22:37 -07:00
Wojciech Nawrocki
c81ee908ea
chore: update stage0
2022-05-12 13:22:37 -07:00
