rel_hom_class

Stream: general

[Yury G. Kudryashov]

I suggest that we split docs#rel_hom_class into order_hom_class and strict_order_hom_class.

[Yury G. Kudryashov]

One will correspond to rel_hom_class (≤) (≤), and the other to rel_hom_class (<) (<).

[Yury G. Kudryashov]

Currently, docs#rel_hom_class.map_inf has unnecessarily strong assumptions (strict_mono instead of monotone) and docs#rel_hom_class.map_sup has gt in TC assumptions.

[Yury G. Kudryashov]

IMHO, both should be changed to order_hom_class, and we should add order_hom_class instances for various rel_homs.

[Yaël Dillies]

Fully agree. This is the plan already.

[Yaël Dillies]

We plan on keeping rel_hom_class and then defining the two order classes you mentioned through abbreviations.

[Yury G. Kudryashov]

You can't do this because of out params