Commit 2023-07-21 16:03 bd0c9574
View on Github →feat: port yaml files from mathlib3 (#6026)
This was done with a locally-hacked version of fix-comments.py, then manually fixing the last 50 or so missing instance names.
This includes CI that verifies the names are valid.