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
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
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
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
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
Wojciech Nawrocki
5cd4bd3552
refactor: auto-derive RpcEncoding
2022-05-12 13:22:37 -07:00
Wojciech Nawrocki
bea68819c9
feat: support optional RPC fields
2022-05-12 13:22:37 -07:00
Wojciech Nawrocki
dd6528bceb
fix: undo incorrect JSON encoding
2022-05-12 13:22:37 -07:00
Sebastian Ullrich
4e3ddf716e
refactor: unnecessary quotation kind
2022-05-12 08:38:09 -07:00
Sebastian Ullrich
75cbb5904e
refactor: use syntax quotations
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
7ad1ccab78
feat: use quotation prechecks where possible at FromToJson
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
9296afca12
chore: undo unnecessary change
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
fbb20d465b
fix: RpcEncoding tests
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
603a062f1f
chore: revert API change
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
63b33424e1
feat: add Widget.Basic
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
460abc4b94
fix: failure in FromToJson
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
0b554f385e
feat: RpcEncoding for inductive types
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
c291a78b6a
fix: repeated field types in RpcEncoding
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
a19c666f2d
feat: add helpers
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
100008ceb1
feat: support generic structure parameters in RpcEncoding
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
72c4717055
chore: remove dead code
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
11e10459bb
refactor: move function to PrettyPrinter
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
81b1f1df6e
refactor: unify format functions
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
aa2ad384e7
chore: remove old InfoTree ctor
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
b33eb12328
chore: simplify evaluation and use macro scope instead of namespace
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
aa5fe5864a
doc: document some Deriving utils
2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
4b3c2b1790
doc: document some meta utilities
2022-05-12 08:38:09 -07:00
Leonardo de Moura
a8032e4173
fix: another mut misbehaving example
...
```
def mutVariableDo2 (list : List Nat) : Nat := Id.run <| do
let mut sum := 0
for _ in list do
sum := sum.add 1 -- first `sum` was not connected, i.e., it was not highlighted when hovering over the second `sum`
pure sum
```
2022-05-12 08:26:07 -07:00
Leonardo de Moura
362961912b
chore: remove unnecessary variable
2022-05-12 06:44:13 -07:00
Leonardo de Moura
f44a701637
chore: style
2022-05-11 15:32:18 -07:00
Sebastian Ullrich
d03f0b3851
fix: set of chained lexical references
2022-05-11 17:32:06 +02:00
Leonardo de Moura
94d2a3ef86
feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures
2022-05-10 18:30:53 -07:00
Leonardo de Moura
c935a3ff6a
feat: improve error location for universe level errors at inductive command
2022-05-10 12:50:01 -07:00
Sebastian Ullrich
392640d292
feat: allow keyword-like projection identifiers
2022-05-10 12:25:30 -07:00
Leonardo de Moura
f58afaaa43
fix: make sure let _ := val and let _ : type := val are treated at letIdDecl
...
closes #1114
2022-05-10 06:52:27 -07:00
Sebastian Ullrich
1b51bab4a1
feat: turn on info trees by default
2022-05-10 06:24:31 -07:00
Leonardo de Moura
7ce0471f28
feat: improve binrel% elaborator
...
It now relies on `binop%` too, and addresses issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387
2022-05-09 18:39:52 -07:00
Leonardo de Moura
1768067aa0
doc: document elaboration issue
...
described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387
TODO: improve `binrel%` elaboration function.
2022-05-09 17:39:24 -07:00
Sebastian Ullrich
ff6537be1b
fix: use consistent goal prefix everywhere
2022-05-09 17:49:00 +02:00
Leonardo de Moura
fc03b2fc31
feat: unfold ident,+
2022-05-09 07:09:53 -07:00
Leonardo de Moura
995d4f0979
chore: prepare for unfold ident,+
2022-05-09 07:09:22 -07:00
Leonardo de Moura
e729b32b2b
feat: unfold should fail if it didn't unfold anything
2022-05-09 06:41:17 -07:00
