## Stream: general

### Topic: cleverer "Try this:"

#### 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?

#### 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.

#### Scott Morrison (Jul 12 2020 at 05:00):

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

#### Scott Morrison (Jul 12 2020 at 05:00):

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

#### Kenny Lau (Jul 12 2020 at 05:02):

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

#### 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

#### 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