two names in "Algebra.Lattice.Properties.BooleanAlgebra" are confusing

[onestruggler]

Hi,

Two names at line 195 in "Algebra.Lattice.Properties.BooleanAlgebra" are confusing:

⊥≉⊤ : ¬ ⊥ ≈ ⊤
⊥≉⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _)

⊤≉⊥ : ¬ ⊤ ≈ ⊥
⊤≉⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _)

It seems better to use "¬⊥≈⊤" and "¬⊤≈⊥" instead.

[jamesmckinna]

(oops, I typed without thinking, and once I had, saw that you were entirely correct... good catch!)

Tagged as bug, because it (appears to) arise from a semantic confusion between ¬ as a propositional connective, and as a field name/algebraic connective...

[Taneb]

...I wrote a whole paragraph defending these names, before double checking myself and finding out that here ¬ is an operator on the elements of the boolean algebra, not a negation of the equality! For that ambiguity, I'd say these names are actually incorrect, and the name of the ¬ operator is possibly worth changing also

[jamesmckinna]

...I wrote a whole paragraph defending these names, before double checking myself and finding out that here ¬ is an operator on the elements of the boolean algebra, not a negation of the equality! For that ambiguity, I'd say these names are actually incorrect,

Snap! hence the hasty deletion of my original response, and its replacement above, together with #2686 . But

...and the name of the ¬ operator is possibly worth changing also

I hadn't got as far as that. What would you call it instead, and how will we manage with the deprecation warnings? Record field names seem 'worse' than ordinary definitions when it comes to renaming, esp. when the warnings don't seem to easily cross module (instantiation) boundaries...

[MatthewDaggitt]

Yup happy to change the names as a short-term win. I think changing the operator name would be much more drastic as @jamesmckinna says...