Zulip Chat Archive

Stream: mathlib4

Topic: resetI


Xavier Roblot (Jan 06 2023 at 07:39):

What is the replacement for resetI in lean4? mathport replaces resetI by skip but that does nothing. In a previous port mathlib4#1309, I declared directly the new instance using haveI but now I have a similar problem in mathlib#1353 (line 276) and I have more difficulties figuring out what I am supposed to do.

Reid Barton (Jan 06 2023 at 08:02):

You should just be able to delete the skips. I think the other errors there are unrelated to resetI.

Xavier Roblot (Jan 06 2023 at 08:30):

Yes, that's probably true in this case but still the question stands since I needed to add the instance manually in mathlib4#1309 and I want to make sure it is the right way to fix that.

Reid Barton (Jan 06 2023 at 08:38):

You don't need resetI ever in Lean 4.

Xavier Roblot (Jan 06 2023 at 08:41):

So what I did in mathlib4#1309 was not correct? It was supposed to work without adding the instance manually?

Reid Barton (Jan 06 2023 at 08:49):

No, that's different--for haveI, you still need either haveI or have.

Mario Carneiro (Jan 06 2023 at 08:55):

mathport is supposed to be deleting skips inserted by this process anyway

Xavier Roblot (Jan 06 2023 at 09:03):

Mario Carneiro said:

mathport is supposed to be deleting skips inserted by this process anyway

It did not in mathlib4#1309 and mathlib#1353. For mathlib#1353, you can still see it on line 276

Mario Carneiro (Jan 06 2023 at 09:13):

oh I see, it's not looking for skip <;> only skip;


Last updated: Dec 20 2023 at 11:08 UTC