Give consistent names to transitivity between strict and non-strict orders

[MatthewDaggitt]

e.g. sometimes in Data.Integer.Properties its ≤-<-trans and in Data.Nat.Properties its <-transʳ.

[jamesmckinna]

The Integer version of the name seems preferable? This may simply be my aversion to primed names, but I think usefully is also more self-documenting.

D'oh 1): on my phone, the superscript looks like a prime!

D'oh 2): I hadn't been aware of issue #1334 before...

[So: perhaps take the following with a pinch of salt...]
But perhaps better would be in Relation.Binary.Definitions to define left- and right- closure of one relation R by another S, with the two lemmas at hand being instances of such concepts...?

D'oh 3): I should look harder at what is already in the library, before posting... 🤦‍♂️

[MatthewDaggitt]

But perhaps better would be in Relation.Binary.Definitions to define left- and right- closure of one relation R by another S, with the two lemmas at hand being instances of such concepts...?

The problem is that the non-strict/strict numeric orders (for various good reasons) aren't usually defined as the closure of one another....

[MatthewDaggitt]

But I agree with your assessment that the first name is better!

[jamesmckinna]

Apologies for potential confusion arising from my

...left- and right- closure of one relation R by another S...

when what I had intended was the property of R being closed (under relational composition) on the left/right by S ie Trans S R R and Trans R S R and wanting to name those, say, Transˡ R S and Transʳ R S... which might in fact suggest the names we should standardise on should be a hybrid of each existing solution, viz. make those definitions and then name the lemmas ≤-<-transʳ etc.?

[MatthewDaggitt]

Ah right, sorry misunderstood! Hmm so we spell out Left and Right in types in full, so it would have to be something like LeftTransitive and RightTransitive, but yes I'm on board!

[jamesmckinna]

Will assign myself... later. I've been doing too much here recently!

[jamesmckinna]

Oh... it seems better to put the relation symbols in suitable left-right order in the name, and use the superscripts, because the directions flip over! PR on way...