Zulip Chat Archive
Stream: general
Topic: fintype_finite
Yaël Dillies (Aug 20 2022 at 10:05):
Why does docs#add_monoid_hom.functions_ext not pass the fintype_finite linter without being registered on #nolints?
Yaël Dillies (Aug 20 2022 at 10:05):
Oh btw could #nolint/#nolints link to https://github.com/leanprover-community/mathlib/blob/master/scripts/nolints.txt ?
Yaël Dillies (Aug 20 2022 at 10:05):
cc @Bryan Gin-ge Chen
Last updated: Dec 20 2023 at 11:08 UTC