Zulip Chat Archive
Stream: general
Topic: Universe linter?
Yury G. Kudryashov (Dec 30 2021 at 04:46):
I've just catched and fixed in #11141 a bug in docs#pi.has_continuous_smul: γ : ι → Type should be γ : ι → Type*. Should we have a linter that forces universe polymorphism?
Last updated: Dec 20 2023 at 11:08 UTC