Issue2788

[JacquesCarette]

This puts back everything that was mistakenly reverted -- closes #2788

[MatthewDaggitt]

Thanks @JacquesCarette!

Was hoping to make the release of v2.3 now, but I guess we need to wait for @jamesmckinna's approval for this.

[jamesmckinna]

Review incoming, but as a placeholder
Re: the additions (x signifies approval):

• Algebra.Construct.Flip.Op
• Data.Fin.Properties
• Data.Sum.Relation.Binary.LeftOrder looks good, but possible downstream refactoring wrt variables
• Data.Sum.Relation.Binary.Pointwise has a spurious anonymous module declaration L111-L114, plus some weirdness in the comment/behaviour wrt variables in ⊎-wellFounded

Re: CHANGELOG
This is trickier, because of the 'anachronism's... will re-review shortly. My suggestions end up still leaving it in a not-completely consistent state!?

[jamesmckinna]

See placeholder comment, plus module-level suggestion.
CHANGELOG comments to follow

[jamesmckinna]

I've only made suggestions... in case my commits make things worse! But CHANGELOG definitely needs fixing, and Pointwise could be (rational reconstruction) tweaked a little from the original, given all the time which has elapsed since the original PR...

[jamesmckinna]

Question: when/if this is merged into the release-2.3 branch, when/how do we also merge it into master? And what about experimental as well?

[JacquesCarette]

If/when this gets merged, we'll have to cherry-pick it, somehow, back onto master and experimental.

[jamesmckinna]

Will re-review in the morning!