Zulip Chat Archive

Stream: new members

Topic: bug with `convert`?


Chris M (Jul 28 2020 at 04:50):

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 (Jul 28 2020 at 05:39):

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 (Jul 28 2020 at 11:43):

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

Kevin Buzzard (Jul 28 2020 at 16:25):

This has been my experience too!


Last updated: Dec 20 2023 at 11:08 UTC