Zulip Chat Archive

Stream: general

Topic: instance `is_trans` on ≤ and <


Damiano Testa (May 23 2021 at 05:25):

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 (May 23 2021 at 07:58):

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

Damiano Testa (May 23 2021 at 08:54):

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

Damiano Testa (May 23 2021 at 10:35):

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


Last updated: Dec 20 2023 at 11:08 UTC