Zulip Chat Archive

Stream: lean4

Topic: Incorrect `fun {a}` linter


Mario Carneiro (Jun 19 2022 at 13:17):

I think a useful linter would be to detect when the proof uses fun {a} => to introduce a variable when fun a => would also have worked. This is usually masking a definition mismatch when you change a forall from implicit to explicit, and the reverse problem (using fun a => where fun {a} => is expected) is a lot worse since it can make variable names not match up


Last updated: Dec 20 2023 at 11:08 UTC