Catalog of porting patterns?

Stream: mathlib4

[Arien Malec]

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]

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

[Patrick Massot]

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

[Arien Malec]

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