Equation Explorer shows Equation4270 wrong

[lyphyser]

It says: "Equation4270[x ◇ (x ◇ x) = x ◇ (y ◇ z)]"

But the equation actually is:
equation 4270 := x ◇ (x ◇ x) = x ◇ (y ◇ y)

The final y has been incorrectly replaced with a z.

[carlini]

It looks like all may be broken. I will take a look to see what's going on soon.

If someone wants to claim+fix this before I get to it plaese do.

[carlini]

equation 953 has been deleted from deleted from AllEquations:

equational_theories/equational_theories/AllEquations.lean

Lines 972 to 975 in b0708a3

	equation 951 := x = y ◇ ((z ◇ x) ◇ (z ◇ x))
	equation 952 := x = y ◇ ((z ◇ x) ◇ (z ◇ y))
	equation 954 := x = y ◇ ((z ◇ x) ◇ (z ◇ w))
	equation 955 := x = y ◇ ((z ◇ x) ◇ (w ◇ x))

I'll bring it back from the dead.

[carlini]

claim

[carlini]

propose PR #481

[goens]

equation 953 didn't disappear, I moved it to Equations.lean in #460

It's still right there where it should:

equational_theories/equational_theories/Equations.lean

Line 83 in b0708a3

equation 953 := x = y ◇ ((z ◇ x) ◇ (z ◇ z))

It shouldn't be moved again, because it's in Chapter 2 of the blueprint (see also the corresponding Zulip thread https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equations.2Elean.20vs.20Chapter.202)

Maybe the script that breaks is not using Equations.lean? (The lean AllEquations file does import it, but if an external script ignores this it might still break)

Also note that this conflicts with #472 and would probably be fixed by that anyway

[goens]

I did just notice that #481 only adds it back as a comment. I guess that works (it's a bit hacky), but we should probably coordinate it with #472 anyway (it's going to conflict)

[carlini]

Yeah, but every other equation that has been removed from AllEquations.lean was removed in this way. I agree it's hacky but it's how things have been done in all the prior cases. Long term plan is to load from a .json file for all scripts that need equation data, that should be done this week I think.

I closed my prior PR because it was put back in the split of AllEquations and have now opened a new PR that'll raise an error if this happens again.

[carlini]

propose PR #491