Zulip Chat Archive

Stream: general

Topic: cleverer "Try this:"


view this post on Zulip Scott Morrison (Jul 12 2020 at 04:28):

Would it be possible for the "Try this:" mechanism to detect by exact X and replace it with just X?

view this post on Zulip Scott Morrison (Jul 12 2020 at 04:28):

I realise this will be a little hacky, but this comes up so often when using by library_search that it seems like it would be kind to new users.

view this post on Zulip Scott Morrison (Jul 12 2020 at 05:00):

https://github.com/leanprover/vscode-lean/pull/207

view this post on Zulip Scott Morrison (Jul 12 2020 at 05:00):

I only did a few tests by hand, but it seems pretty straightforward.

view this post on Zulip Kenny Lau (Jul 12 2020 at 05:02):

a problem, though, is that sometimes by exact X works but not X

view this post on Zulip Mario Carneiro (Jul 12 2020 at 05:11):

Well the Try this replacement was never foolproof in the first place, so I don't think this is a major worry

view this post on Zulip Scott Morrison (Jul 12 2020 at 05:32):

It also conspicuously screws up if you just write begin library_search end (without any commas), as it deletes the end.


Last updated: May 11 2021 at 00:31 UTC