Implement ≤-total in terms of _≤?_

[Taneb]

Fixes #2436

[gallais]

You'll need a CHANGELOG entry as it's a breaking change for people
who are relying on ≤-total's reduction behaviour on open terms.

[Taneb]

That's a good point, I'll add a changelog after #2439 gets merged

[JacquesCarette]

I'll wait to do a proper review once the CHANGELOG is in place.

[jamesmckinna]

Modulo:

• CHANGELOG
• breaking

This looks great!

[jamesmckinna]

How does this PR contribute to (positively or negatively...) the issues about 'concrete' orderings raised in issue #1179 ?
It seems as though both are trying to tackle a pervasive problem; this PR, locally, with the bigger issue at a (more) global level.

[Taneb]

@jamesmckinna they're related, but I don't think either of them solve or get in the way of the other

[jamesmckinna]

Happy to merge once there's a second 'approve' review from one of the other maintainers... and a CHANGELOG entry ;-)

[jamesmckinna]

I think when you resolve the merge conflict in CHANGELOG, you'll see that your note on this being a non-backwards compatible change has been added to the v2.1 version, and you should bring the whole of that file up-to-date with the current master/v2.2 version...?

[MatthewDaggitt]

The question is do we view this as a backwards compatible breaking change? If it was just a change in behaviour then I would say yes and bump it to v3.0. If however, we argue that this is in fact a performance bug then the maybe we can justify adding it to v2.2?

[Taneb]

@MatthewDaggitt while I would like it in sooner, of course, the position that has the better argument is that we don't make any performance guarantees at all (our readme says more or less this right near the beginning). Based on that, it probably ought wait for 3.0

[jamesmckinna]

@MatthewDaggitt while I would like it in sooner, of course, the position that has the better argument is that we don't make any performance guarantees at all (our readme says more or less this right near the beginning). Based on that, it probably ought wait for 3.0

Well, if you were to make that sacrifice, that would ease the path to a v2.2 release following #2473 ...