Zulip Chat Archive

Stream: general

Topic: algebraic normalizer


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 22 2019 at 00:35):

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


Last updated: May 13 2021 at 18:26 UTC