Zulip Chat Archive

Stream: mathlib4

Topic: Catalog of porting patterns?


Arien Malec (Nov 16 2022 at 16:56):

Is there a catalog of typical porting patterns & heuristics? Some of the heuristics @Scott Morrison applied in the video, the #align questions @Kevin Buzzard has been asking, etc?

Would be useful to have a place where one could ask questions, capture patterns/heuristics, and get a documentation asset created over time...

Ruben Van de Velde (Nov 16 2022 at 17:00):

I'd say it should be on https://github.com/leanprover-community/mathlib4/wiki

Patrick Massot (Nov 16 2022 at 17:00):

It is meant to be https://github.com/leanprover-community/mathlib4/wiki

Arien Malec (Nov 16 2022 at 17:03):

Ah, of course. So if I come across a situation not in that catalog, I'll ask away...


Last updated: Dec 20 2023 at 11:08 UTC