Zulip Chat Archive

Stream: general

Topic: algebraic normalizer


Jesse Michael Han (Feb 21 2019 at 20:23):

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

Mario Carneiro (Feb 22 2019 at 00:31):

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 (Feb 22 2019 at 00:32):

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 (Feb 22 2019 at 00:35):

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


Last updated: Dec 20 2023 at 11:08 UTC