## Stream: new members

### Topic: library_search bug?

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


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

#### Johan Commelin (Jul 19 2020 at 05:30):

@Chris M Please remove the by before library_search.

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


#### Scott Morrison (Jul 19 2020 at 06:40):

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

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

#### Chris M (Jul 21 2020 at 04:05):

Worked, thanks!

Last updated: May 11 2021 at 13:22 UTC