cleverer "Try this:"

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Scott Morrison]

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