library_search bug?

Stream: new members

[Chris M]

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?

[Bryan Gin-ge Chen]

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

[Johan Commelin]

@Chris M Please remove the by before library_search.

[Bryan Gin-ge Chen]

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

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Chris M]

Worked, thanks!