Zulip Chat Archive

Stream: general

Topic: lintsprint 8 Oct

Johan Commelin (Oct 08 2020 at 04:20):

https://leanprover-community.github.io/mathlib_stats/nolints.png
Just look at that graph!

Aaron Anderson (Oct 08 2020 at 05:26):

computability/halting #4524

Aaron Anderson (Oct 08 2020 at 05:34):

multiset/pi #4526

Johan Commelin (Oct 08 2020 at 10:04):

#4531 lints data/padics/* but also does some squeeze_simp speed-up. So I didn't label it lintfix

Heather Macbeth (Oct 08 2020 at 15:58):

I was thinking of doing a PR with @[nolint has_inhabited_instance] for some instances that represent injective or bijective functions with decoration. Here are the examples I was thinking of covering. Does this seem reasonable?
docs#function.embedding
docs#homeomorph
docs#isometric

Heather Macbeth (Oct 08 2020 at 16:33):

OK, the above done as #4541
This covers:
topology/homeomorph
topology/metric_space/isometry
and one of several errors in
logic/embedding

Last updated: Dec 20 2023 at 11:08 UTC