Faster elaboration of AllEquations

Stream: Equational

[Joachim Breitner]

Processing of AllEquations.lean was slow (70s on my machine!) and the bottle neck was type class inference.

In equational#52 I introduce syntax

equation 10 := x = x ∘ (y ∘ x)

which is more concise but, more importantly, elaborates more directly and avoiding instance synthesis, so the file now compiles in 10s. Much more usable.

[Terence Tao]

[deleted]

[Joachim Breitner]

In the interest of moving fast I’ll just merge this, futher clean-up and refinement can happen separately, unless someone stops me right away :-)

[Terence Tao]

Will this require a (slight) refactoring of Subgraph.lean and Equations.lean to use the new notation?

[Joachim Breitner]

No, it’s really just a macro that expands to the same definition of the Equation123. No downstream effects.

[Joachim Breitner]

Equations.lean can use the notation. It’s not pressing (as that file is small). But for consistency maybe it should use it. But actually, for understanding what’s going on it’s actually nicer to spell it out there using well-known lean syntax. We can revise later.