instance `is_trans` on ≤ and <

Stream: general

[Damiano Testa]

Dear All,

playing around with orders, I noticed that the instance below are missing. I imagine that this is on purpose. Why are they not instance?

Thanks!

variables {α : Type*} [preorder α]

instance : is_refl α (≤) :=
{ refl := λ a, le_of_eq rfl }

instance : is_trans α (≤) :=
{ trans := λ a b c, le_trans }

instance : is_trans α (<) :=
{ trans := λ a b c, lt_trans }

[Eric Wieser]

Are you sure those are missing? I think docs#has_le.le.is_preorder provides them

[Damiano Testa]

Ah, maybe I was missing an import. I will try once I am back at a computer, thanks!

[Damiano Testa]

Eric, I just checked and adding import order.rel_classes, the instances are there. Thanks!