resetI

Stream: mathlib4

[Xavier Roblot]

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]

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

[Xavier Roblot]

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]

You don't need resetI ever in Lean 4.

[Xavier Roblot]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Xavier Roblot]

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]

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