Zulip Chat Archive

Stream: new members

Topic: lemma naming


view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jul 26 2020 at 10:21):

What else could not_true_iff be?

view this post on Zulip 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).

view this post on Zulip 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