Zulip Chat Archive
Stream: mathlib4
Topic: Isolated by
Yaël Dillies (May 21 2023 at 13:51):
Could we get rid of the "isolated by" linter? I have an isolated by here that I cannot unisolate.
Eric Wieser (May 21 2023 at 18:01):
I don't see what you mean, the linter doesn't seem to be complaining?
Mario Carneiro (May 21 2023 at 18:19):
you could line-break the statement more
Last updated: Dec 20 2023 at 11:08 UTC