lemma naming

Stream: new members

[Chris M]

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]

What else could not_true_iff be?

[Chris M]

Well this is a trivial example, so maybe nothing else (though parsing it would still be faster for my brain).

[Sebastien Gouezel]

That's the goal of a good name: no ambiguity, but short if possible as long statement are in fact harder to read.