bug with `convert`?

Stream: new members

[Chris M]

I have the following code:

import data.real.basic
import tactic

open function
open nat
variables n:ℕ
example (e : prime (2 * n + 1) ) : prime (n + n + 1) :=
begin
  convert e using 0,
end

This code produces two goals that are identical:
https://gyazo.com/c1b7de50bace99c0d332881e94985659

I'm guessing this is a bug?

[Alex J. Best]

I guess its a slight bug, do you have a more realistic use case (In this case you'd just do convert e or convert e using 2 right).

[Jalex Stark]

In my experience, I can only get convert to give me two identical goals in cases where those goals are useless

[Kevin Buzzard]

This has been my experience too!