Inf on ordinal

Stream: maths

[Sebastien Gouezel]

I can't find an has_Inf instance on ordinal.{u}. Is there already a canonical way to talk of the smallest ordinal in a set of ordinals (which makes sense as this is well ordered)? @Mario Carneiro , maybe.

[Mario Carneiro]

@Sebastien Gouezel There is an indexed min function, but it's not an instance of anything

[Mario Carneiro]

see docs#ordinal.min and docs#ordinal.omin

[Mario Carneiro]

I guess omin could be a has_Inf instance

[Sebastien Gouezel]

Thanks. I'll build a conditionally_complete_linear_order instance with that.