Zulip Chat Archive
Stream: general
Topic: Feature request: rcases try this
Yury G. Kudryashov (May 14 2020 at 00:46):
When I want to run rcases on a nontrivial structure, sometimes it's hard to get the with pattern right. It would be nice to ask rcases for a pattern of depth n, get a pattern, then fix variable names.
Mario Carneiro (May 14 2020 at 00:46):
rcases?
Yury G. Kudryashov (May 14 2020 at 00:47):
Shame on me
Yury G. Kudryashov (May 14 2020 at 00:48):
Next time I should try before asking
Kevin Buzzard (May 14 2020 at 06:34):
It just shows that it's getting hard to keep up, which is a good thing :-) I think rcases? is relatively new.
Johan Commelin (May 14 2020 at 06:36):
Nope, has been around for ages.
Kevin Buzzard (May 14 2020 at 06:38):
ha ha, maybe it just shows that I can't keep up :-)
Patrick Massot (May 14 2020 at 08:13):
https://github.com/leanprover-community/mathlib/commit/732ec0efaca37955bf08d656f1b47a065d45bf7f August 8th 2018
Mario Carneiro (May 14 2020 at 08:16):
Original zulip chat. I was curious if Kevin originally requested the feature :)
Patrick Massot (May 14 2020 at 08:18):
I think it was me
Patrick Massot (May 14 2020 at 08:19):
Yes it was
Yury G. Kudryashov (May 14 2020 at 09:04):
So, for me it was always there. I wonder how I've missed it.
Jeremy Avigad (May 14 2020 at 18:36):
I didn't know about it either. It's a nice feature.
Along these lines: in VS Code, when you hover over a definition of tactic with a really big docstring, the text gets clipped. I suppose the best thing to do in that case is use "Peek definition" and read the comment in the source?
Johan Commelin (May 14 2020 at 18:37):
Yes, I find this annoying as well. It would be great if hover text could be shown in a dedicated frame
Johan Commelin (May 14 2020 at 18:37):
E.g. 4 or 5 lines horizontally at the bottom of the screen, with scroll bar.
Bryan Gin-ge Chen (May 14 2020 at 18:51):
I guess it's not the most ergonomic thing, but I've gotten used to carefully moving my pointer over the hover and then scrolling down to see the rest of the docstring. Or are there some docstrings that are too long even for this?
Johan Commelin (May 14 2020 at 18:52):
This works for me around 53% of the time...
Johan Commelin (May 14 2020 at 18:52):
The rest of the time, the hover simply disappears
Jeremy Avigad (May 15 2020 at 15:32):
Same with me. I think I figured out the trick: if you move from the word you are hovering over to the window quickly enough, the window doesn't disappear and you can scroll. I think it is a timing thing.
Last updated: Dec 20 2023 at 11:08 UTC