algebraic normalizer

Stream: general

[Jesse Michael Han]

What is the algebraic normalizer, what does it do, and why are some things in mathlib tagged with the [@algebra] attribute?

[Mario Carneiro]

The algebraic normalizer is a project that leo planned on building for years and never got around to. I'm not sure but it might even be one of the stretch goals for lean 4

[Mario Carneiro]

The @[algebra] attribute is part of some trickery for using typeclass inference on extremely vague patterns, like ?m1 ?m2 ?m3. I'm not sure how or to what extent it works currently

[Mario Carneiro]

see https://github.com/leanprover/lean/wiki/Refactoring-structures