Distributivity lemmas

Stream: general

[Yaël Dillies]

I am quite unhappy with the current naming convention for distributivity lemmas. Consider

• and_or_distrib_left
• or_and_distrib_left
• and_or_distrib_right
• or_and_distrib_right

Which says what? I never know.
Could we make it so that the thing which distributes is always in the same place relative to what is distributed?

[Kyle Miller]

Isn't it that foo_bar_distrib_left is that a foo (b bar c) = (a foo b) bar (a foo c) and foo_bar_distrib_right is (a foo b) bar c = (a bar c) foo (b bar c)?

[Yaël Dillies]

Yeah, so names which are at Hamming distance one do not correspond to lemmas which are at Hamming distance one.