classes: extends vs assumption

Stream: maths

[Jakub Kądziołka]

linear_order is defined as extends partial_order, which means that one can ask for a linear_order \a without first specifying [preorder \a] [partial_order \a].

However, this is not always done. For example, succ_order and is_succ_archimedean don't do so:

@[ext] class succ_order (α : Type*) [preorder α] := ...
class is_succ_archimedean (α : Type*) [preorder α] [succ_order α] : Prop := ...

This means that to use them, you need to say [preorder \a] [succ_order \a] [is_succ_archimedean \a]. Is there a reason extends is not used in this case?

[Yaël Dillies]

The latter case is called a "mixin". I could've very well made is_succ_archimedean extend succ_order, but at the time I thought we would have a few other incompatible possible extensions. I'm not sure this will happen anymore.