Stream: new members
Topic: lemma naming
Chris M (Jul 26 2020 at 10:18):
It seems to me that lemma naming conventions are not as informative as they could be. e.g.
not_true_iff : ¬true ↔ false. Wouldn't it be better if this was called
not_true_iff_false : ¬true ↔ false? It would make the names longer but much easier to understand, which seems to me like it's worth it.
Sebastien Gouezel (Jul 26 2020 at 10:21):
What else could
Chris M (Jul 26 2020 at 10:25):
Well this is a trivial example, so maybe nothing else (though parsing it would still be faster for my brain).
Sebastien Gouezel (Jul 26 2020 at 10:26):
That's the goal of a good name: no ambiguity, but short if possible as long statement are in fact harder to read.
Last updated: May 12 2021 at 04:19 UTC