Zulip Chat Archive

Stream: new members

Topic: library_search bug?


view this post on Zulip Chris M (Jul 19 2020 at 05:20):

I'm running the following code:

import data.real.basic
import tactic

lemma my_lemma2 :  {x y ε : },
  0 < ε  ε  1  abs x < ε  abs y < ε  abs (x * y) < ε :=
begin
  intros x y ε epos ele1 xlt ylt,
  have h:abs y  0, {by library_search}
end

The  `library_search` suggests:  `Try this: exact abs_nonneg y`. However, when I click it, it just produces `abs_nonneg y`, without the `exact`. It's not a big problem but I presume this is a bug?

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 05:27):

Yeah, VS Code isn't smart enough to realize that the have is followed by a comma, which requires something in tactic mode to follow it, rather than something in term mode. (If you use := it would work). I think @Scott Morrison added this feature (where the replacement tries to avoid putting in exact).

view this post on Zulip Johan Commelin (Jul 19 2020 at 05:30):

@Chris M Please remove the by before library_search.

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 05:41):

I didn't realize we could use by in tactic mode!

example : true :=
begin
  by by by by by by by trivial
end

view this post on Zulip Scott Morrison (Jul 19 2020 at 06:40):

This is more of a VSCode "Try this:" bug than library_search.

view this post on Zulip Scott Morrison (Jul 19 2020 at 06:40):

I think the correct fix is indeed: don't use unnecessary bys in tactic mode if you want the "Try this:" feature to work. Automatically detecting unnecessary by sounds hard.

view this post on Zulip Chris M (Jul 21 2020 at 04:05):

Worked, thanks!


Last updated: May 11 2021 at 13:22 UTC