Sebastian Ullrich
|
0f6e6c8a51
|
chore: update stage0
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
b585b2251e
|
fix: adapt to stricter grammar
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
ce054fb2e7
|
fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
7a3ee51d05
|
doc: missing word
|
2022-06-16 10:12:07 +02:00 |
|
Mariana Alanis
|
198179d0cc
|
fix: add a better handling in case only worker crashes (apply CR comments)
|
2022-06-15 18:40:44 -07:00 |
|
Mariana Alanis
|
e61799a77f
|
fix: add a better handling in case only worker crashes (CR comments)
|
2022-06-15 18:40:44 -07:00 |
|
Mariana Alanis
|
30f3d6f82d
|
fix: add a better handling in case only worker crashes (CR comments)
|
2022-06-15 18:40:44 -07:00 |
|
Mariana Alanis
|
4d7d82af86
|
fix: add a better handling in case only worker crashes (CR comments)
|
2022-06-15 18:40:44 -07:00 |
|
Mariana Alanis
|
b0f9754e0f
|
fix: add a better handling in case only worker crashes
|
2022-06-15 18:40:44 -07:00 |
|
Mariana Alanis
|
6b75ca9734
|
fix: add a better handlng in case only worker crashes (and server stays available)
|
2022-06-15 18:40:44 -07:00 |
|
Leonardo de Moura
|
d2888a49d7
|
chore: remove old hack that is not needed anymore
|
2022-06-15 16:36:54 -07:00 |
|
Leonardo de Moura
|
3228db29dd
|
chore: use double ticks
|
2022-06-15 07:17:17 -07:00 |
|
Sebastian Ullrich
|
524ae5abf7
|
chore: CI: purge ccache
|
2022-06-15 13:39:24 +02:00 |
|
Sebastian Ullrich
|
23d157a3ff
|
chore: remove dead code
|
2022-06-15 12:43:59 +02:00 |
|
Sebastian Ullrich
|
bfce841985
|
chore: update stage0
|
2022-06-15 10:01:47 +02:00 |
|
Leonardo de Moura
|
5896e6f1d6
|
chore: fix docs
|
2022-06-14 17:35:33 -07:00 |
|
Leonardo de Moura
|
540e9e85f3
|
chore: update release notes
|
2022-06-14 17:31:26 -07:00 |
|
Leonardo de Moura
|
989d8f04e1
|
chore: fix tests
|
2022-06-14 17:27:13 -07:00 |
|
Leonardo de Moura
|
f6d1e48cb8
|
fix: constant => opaque issues
|
2022-06-14 17:19:54 -07:00 |
|
Leonardo de Moura
|
fb55ec29e1
|
chore: update stage0
|
2022-06-14 17:14:44 -07:00 |
|
Leonardo de Moura
|
22c8f10b12
|
chore: remove constant command
|
2022-06-14 17:14:28 -07:00 |
|
Leonardo de Moura
|
02c4e548df
|
feat: replace constant with opaque
|
2022-06-14 17:02:59 -07:00 |
|
Leonardo de Moura
|
ac33193b30
|
chore: update stage0
|
2022-06-14 16:45:20 -07:00 |
|
Leonardo de Moura
|
3b259afaf0
|
chore: fix tests
|
2022-06-14 16:43:22 -07:00 |
|
Leonardo de Moura
|
346c4beb70
|
feat: elaborate opaque command
|
2022-06-14 16:36:24 -07:00 |
|
Leonardo de Moura
|
794021b9e4
|
chore: adjust codebase
`opaque` is now a command keyword
|
2022-06-14 16:32:53 -07:00 |
|
Leonardo de Moura
|
5193c6d0ef
|
chore: update stage0
|
2022-06-14 16:23:49 -07:00 |
|
Leonardo de Moura
|
05778565ab
|
feat: add opaque command
It will replace the `constant` command. See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20is.20.60opaque.60.3F/near/284926171
|
2022-06-14 16:22:36 -07:00 |
|
Jakob von Raumer
|
d7cb93e9e4
|
feat: allow conv mode's arg command to access implicit arguments
|
2022-06-14 16:15:38 -07:00 |
|
Leonardo de Moura
|
d78e7cd011
|
feat: macro expand cases and induction tactics multiple LHSs
|
2022-06-14 14:18:52 -07:00 |
|
Leonardo de Moura
|
3a1dc5e066
|
fix: support new inductionAlt syntax at Linter/Basic.lean
|
2022-06-14 11:31:49 -07:00 |
|
Leonardo de Moura
|
bd2cccf287
|
chore: use double tick
|
2022-06-14 11:30:55 -07:00 |
|
Leonardo de Moura
|
2dad133208
|
chore: update stage0
|
2022-06-14 11:26:06 -07:00 |
|
Leonardo de Moura
|
daeb271678
|
feat: update induction and cases syntax
We can now write
```
induction x with
| foo | bar => ...
| boo => ...
```
TODO: expand alternatives containing multiple LHSs.
|
2022-06-14 11:25:15 -07:00 |
|
Leonardo de Moura
|
05a72a9e00
|
chore: update stage0
|
2022-06-14 11:17:33 -07:00 |
|
Leonardo de Moura
|
7c9b5b7147
|
feat: prepare to support multi-cases at cases and induction
We want to be able to write
```
induction x with
| foo | bar => ...
| boo => ...
```
|
2022-06-14 11:16:58 -07:00 |
|
Sebastian Ullrich
|
43b08239b0
|
fix: further conv goal state refinements
|
2022-06-14 11:09:47 +02:00 |
|
Sebastian Ullrich
|
7bb94abb62
|
feat: trace.Elab.input
Unlike Elab.command, it does not contain macro expansions
|
2022-06-14 10:41:56 +02:00 |
|
Leonardo de Moura
|
77ae79be46
|
chore: use let/if in do blocks
|
2022-06-13 17:10:14 -07:00 |
|
Leonardo de Moura
|
7dbdfa090a
|
chore: remove debugging leftovers
|
2022-06-13 16:37:31 -07:00 |
|
E.W.Ayers
|
13e286f545
|
doc: fix docstring for InteractiveGoal
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
2edf02544e
|
chore: rm ExprWithCtx
We will make this a separate PR
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
367bde3601
|
chore: revert "refactor: replace InfoWithCtx with ExprWithCtx"
This reverts commit db342793d53c986b8794084196552c33711f9091.
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
f64cb95eca
|
refactor: replace InfoWithCtx with ExprWithCtx
This is potentially controversial. There are still some [todo]s that need sorting.
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
3d561a3ab0
|
doc: add docstrings for interactive
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
e3d2080232
|
refactor: PPExprTaggedRequest -> PPExprTaggedParams
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
fd66e70d1e
|
fix: explicit structure for PPExprTaggedRequest
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
69facfbe8e
|
fix: remove Optional from InteractiveHypothesisBundle.fvarIds
|
2022-06-13 16:32:01 -07:00 |
|
E.W.Ayers
|
45e3c72be7
|
refactor: InteractiveHypothesis → InteractiveHypothesisBundle
|
2022-06-13 16:32:01 -07:00 |
|
Ed Ayers
|
5130da82a8
|
doc: src/Lean/Widget/InteractiveGoal.lean
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
|
2022-06-13 16:32:01 -07:00 |
|