Leonardo de Moura
ee6e2036dd
feat: allow relations in Type at Trans
...
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Calc.20mode/near/291214574
2022-07-28 10:13:01 -07:00
Leonardo de Moura
d0d5effcbc
doc: update doc string
2022-07-28 09:48:46 -07:00
Sebastian Ullrich
556358e84c
chore: Nix: better solution for filtering test output
2022-07-28 17:12:17 +02:00
Wojciech Nawrocki
e7f91d2d01
feat: forward all args to server
2022-07-28 15:58:32 +02:00
Wojciech Nawrocki
2744f94ff5
fix: forward memory and stack sizes to server
2022-07-28 15:58:32 +02:00
Leonardo de Moura
10c49d0007
fix: preserve user-facing names and BinderInfo when lifting let-rec declarations
...
closes #1377
2022-07-28 06:36:45 -07:00
Siddharth
a9e22a5119
doc: src/Lean/Declaration.lean ( #1330 )
...
* doc: Add explanations to MetavarContext
The explanations were taken from Leo's talk at the ICERM
Mathlib porting hackathon.
* doc: Add documentation for Declaration
This is explanations taken from Leo's talk given
at the post ICERM Mathlib porting hackathon.
* Update src/Lean/Declaration.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* Update src/Lean/Declaration.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* Update src/Lean/MetavarContext.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* fix depth comment
Co-authored-by: Scott Morrison <scott@tqft.net>
2022-07-27 19:46:11 -07:00
Leonardo de Moura
b5ad9bd4e2
chore: update stage0
2022-07-27 19:38:19 -07:00
Leonardo de Moura
6db01d8e48
perf: simpler isDefEq caching
...
We don't try to reuse the cache contents between different `isDefEq`
calls. Thus, we can cache more results and ignore whether the state of
the metavariable context affects them or not.
Closes #1102
2022-07-27 19:35:45 -07:00
Leonardo de Moura
654a4b0478
fix: add term info at trailing parsers
2022-07-27 18:10:46 -07:00
Leonardo de Moura
388163e023
doc: add some doc strings
2022-07-27 18:02:47 -07:00
Leonardo de Moura
6dcba78338
refactor: improve MVarId method discoverability
...
See issue #1346
2022-07-27 17:49:00 -07:00
Leonardo de Moura
d267b38a91
fix: disable "error to sorry" and "error recovery" at failIfSuccess
...
closes #1375
2022-07-27 17:09:34 -07:00
Leonardo de Moura
888dba815d
chore: update stage0
2022-07-27 16:10:38 -07:00
Leonardo de Moura
49ce4408df
feat: validate parametric local instances
...
Closes #1373
2022-07-27 16:09:56 -07:00
Leonardo de Moura
c210781af8
refactor: add doc strings, cleanup, and dotted notation friendly API
...
See #1346
2022-07-27 16:01:15 -07:00
Leonardo de Moura
00dd9da304
chore: update stage0
2022-07-27 13:41:21 -07:00
Leonardo de Moura
1c770ac8d7
feat: doc strings for declare_syntax_cat
...
see #1374
2022-07-27 13:40:08 -07:00
Leonardo de Moura
1bf53e4fc9
doc: add doc strings for let parsers
2022-07-27 10:56:44 -07:00
Leonardo de Moura
3363ee414b
doc: add doc strings for declarations added by the init_quot command
...
See #1374
2022-07-27 10:17:03 -07:00
Leonardo de Moura
54c5436efb
chore: update stage0
2022-07-27 10:00:57 -07:00
Leonardo de Moura
a7e0976ae6
chore: style
2022-07-27 09:58:52 -07:00
Leonardo de Moura
92d360353c
feat: elaborate add_decl_doc
2022-07-27 09:58:49 -07:00
Leonardo de Moura
5f55422bc2
chore: update stage0
2022-07-27 09:31:53 -07:00
Leonardo de Moura
2c0de29dfd
feat: add add_decl_doc command
2022-07-27 09:30:32 -07:00
Leonardo de Moura
0d43684956
chore: fix some docstrings
2022-07-27 06:46:00 -07:00
Leonardo de Moura
97a5a88ae2
doc: add doc string to simp attribute parser
2022-07-27 06:34:55 -07:00
Leonardo de Moura
c53c4413c4
feat: add doc string to user-defined simp attribute parser
...
see #1374
2022-07-27 06:13:10 -07:00
Leonardo de Moura
635752dd2c
feat: add info node from attributes to their parsers
...
see #1374
2022-07-27 06:12:43 -07:00
Leonardo de Moura
ba24f7f57a
chore: update stage0
2022-07-26 18:51:10 -07:00
Leonardo de Moura
ed7f502e54
feat: doc string support for register_simp_attr, register_option, register_builtin_option, declare_config_elab
...
see #1374
2022-07-26 18:46:23 -07:00
Leonardo de Moura
3e7d45aaba
fix: improve finer-grained term infos for do blocks
...
see #1248
This commit adds a small hack to fix the term info for the following `do`-elements
```lean
let (x, y) := ...
let (x, y) ← ...
let mut (x, y) ← ...
let some x ← ... | ...
```
2022-07-26 18:18:05 -07:00
Leonardo de Moura
fffd61cf98
chore: update stage0
2022-07-26 17:56:49 -07:00
Leonardo de Moura
642cf0bc6d
feat: add option pp.showLetValues
...
closes #1345
2022-07-26 17:53:34 -07:00
Leonardo de Moura
0e3f031660
fix: position information for with_annotate_term when coercions are used
...
see #1248
2022-07-26 16:09:45 -07:00
Leonardo de Moura
c22120371e
feat: finer-grained term infos for do blocks
...
closes #1248
2022-07-26 15:47:37 -07:00
Leonardo de Moura
bbad6d1efe
feat: add with_annotate_term
2022-07-26 15:13:28 -07:00
Leonardo de Moura
43c787d1c6
feat: synthesize implicit structure fields in the structure instance notation
...
closes #1305
2022-07-26 13:24:57 -07:00
Leonardo de Moura
e68e448070
fix: convert inductive type instance implicit parameters to implicit when building SizeOf instance
...
It is better for TC resolution since the parameter can be inferred by
typing constraints, and it addresses issue #1373
2022-07-26 12:42:47 -07:00
Leonardo de Moura
642b30ab47
feat: add withInstImplicitAsImplict
2022-07-26 12:35:30 -07:00
Leonardo de Moura
d6f0880d11
feat: add option warningAsError
2022-07-26 05:57:54 -07:00
Leonardo de Moura
385cfa6001
fix: fixes #1372
2022-07-26 05:51:02 -07:00
Leonardo de Moura
3896244c55
chore: cleanup
2022-07-25 22:39:56 -07:00
Leonardo de Moura
30199745ad
chore: update stage0
2022-07-25 22:19:59 -07:00
Leonardo de Moura
90fb110cc9
refactor: improve FVarId method discoverability
...
See issue #1346
2022-07-25 22:18:58 -07:00
Leonardo de Moura
db7e546155
fix: Match.unify?
...
closes #1361
2022-07-25 20:30:01 -07:00
Leonardo de Moura
b3b2a07ed0
feat: support dotted notation and named arguments in patterns
2022-07-25 18:19:32 -07:00
Leonardo de Moura
69b7771570
fix: etaArgs and ellipsis at elabAppArgs
...
When `..` is used, we should not eta-expand but add `_`s.
2022-07-25 18:13:32 -07:00
Leonardo de Moura
aa267dbc9b
doc: add doc-strings
2022-07-25 17:36:10 -07:00
Leonardo de Moura
c418e8d2c5
fix: use useExplicit := false when processing instance ... where ... notation fields
...
See new test.
2022-07-25 16:53:13 -07:00
