Zulip Chat Archive
Stream: toric
Topic: Mathlib linters
Yaël Dillies (Mar 05 2025 at 12:17):
Heads up that I've just turned the mathlib linters on in Toric. You will now see warnings pop up as you edit the code. Please make sure your code produces as few warnings as possible!
Paul Lezeau (Mar 05 2025 at 14:49):
Nice!
Last updated: Dec 20 2025 at 21:32 UTC