Remove `bigmaxr` from `Rstruct.v`?

Open affeldt-aist opened this issue 2 months ago • 4 comments

https://github.com/math-comp/analysis/blob/3b30884c4a9134f8c98cfab47c9cfa7f6fd4db0d/reals_stdlib/Rstruct.v#L551

as discussed in the conversation of PR https://github.com/math-comp/analysis/pull/1736

@t6s @CohenCyril

Oct 24 '25 03:10 affeldt-aist

What is the candidate replacement for this bigmaxr?

Oct 24 '25 07:10 CohenCyril

The bigmax offered by order.v.

Oct 24 '25 08:10 affeldt-aist

Ok, then it's not 100% clear for that the bigmaxr can actually be subsumed without overhead (because of head x r in its definition), I think one needs to try and see.

Oct 24 '25 08:10 CohenCyril

Yes, indeed. That's why we kept it for a while with a deprecation comment inviting to look at order.v. The full story is that with @drouhling we actually tried both approaches and concluded (iirc) that the one with head x r was harder to use. But that was a long time ago, maybe it's time to let it go? :-(

Oct 24 '25 08:10 affeldt-aist