Tentative sub_porderType

[hivert]

Dear Barbichu,

I started working with your order.v file and I realized that there are some missing construction. I'm willing to contribute, but I'm really scared by all these Canonical tricks. In particular, in my code, I didn't manage to have a proper working double inheritance from finType and pordType. That why I'd like to use yours.

Here are a few contributions I'm offering to adapt to your code and contribute provided I manage to get them right. I'm already using them intensively in my code. 1- A subtype of a porderType / orderType are also porderType / orderType. I'd like to provide the generic construction. My typical use cases are ordinals 'I_n. and tuple with the lex order. 2- If T is a totally ordered type then lexi is also total (eg: seq nat). 3- The theory of monotonic maps (should we call them order morphism ?) eg: the val map from a subordtype, the compose of two monotonic map is monotonic, strict monotonic map are injective.

I just wrote a tentative code to solve my first point, but I'm not sure I'm on the right path. It worked for my use cases but maybe I'm missing some kind of inheritance which will become problematic.

So my questions are:

• could you have a look at my code to tell me if its the right way, I'll then complete it.
• please share any comment on the three proposals above. In particular, do you think they fits in your file ?

Regards,

Florent

PS: I case it's not obvious: I don't consider the code in this pull request as ready to be merge. Also if you don't think pull request is the right workflow for that, please tell me what you think is better.

[affeldt-aist]

Is this PR still under consideration?

[hivert]

Is this PR still under consideration?

I guess this is completely outdated and should be closed.