Zulip Chat Archive

Stream: general

Topic: Feature request: rcases try this


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 14 2020 at 00:46):

rcases?

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 00:47):

Shame on me

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 00:48):

Next time I should try before asking

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 14 2020 at 06:36):

Nope, has been around for ages.

view this post on Zulip Kevin Buzzard (May 14 2020 at 06:38):

ha ha, maybe it just shows that I can't keep up :-)

view this post on Zulip Patrick Massot (May 14 2020 at 08:13):

https://github.com/leanprover-community/mathlib/commit/732ec0efaca37955bf08d656f1b47a065d45bf7f August 8th 2018

view this post on Zulip Mario Carneiro (May 14 2020 at 08:16):

Original zulip chat. I was curious if Kevin originally requested the feature :)

view this post on Zulip Patrick Massot (May 14 2020 at 08:18):

I think it was me

view this post on Zulip Patrick Massot (May 14 2020 at 08:19):

Yes it was

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 09:04):

So, for me it was always there. I wonder how I've missed it.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 14 2020 at 18:37):

E.g. 4 or 5 lines horizontally at the bottom of the screen, with scroll bar.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 14 2020 at 18:52):

This works for me around 53% of the time...

view this post on Zulip Johan Commelin (May 14 2020 at 18:52):

The rest of the time, the hover simply disappears

view this post on Zulip 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: May 16 2021 at 20:13 UTC