## Stream: general

### Topic: is_well_order

#### Floris van Doorn (Mar 13 2019 at 18:33):

What is the reason that is_well_order is used in the library (for example for ordinals), but that it doesn't extend the other order structures, like linear order? Why is it used in instead of having an argument [well_order α] which extends linear_order?

#### Mario Carneiro (Mar 13 2019 at 18:35):

it's less easy to deal with linear_order objects as if they were just relations

#### Mario Carneiro (Mar 13 2019 at 18:36):

also I had some issues with the fact that the hierarchy was built on le instead of lt

#### Mario Carneiro (Mar 13 2019 at 18:36):

at least, that's what I remember

#### Floris van Doorn (Mar 13 2019 at 18:37):

well, most classes in the hierarchy have both le and lt, right?
If I want to use lemmas about linear_order, is the nicest thing to do just to have a local instance?

#### Mario Carneiro (Mar 13 2019 at 18:56):

yeah, that's what I do in the ordinal proofs

#### Mario Carneiro (Mar 13 2019 at 18:56):

there is a function for that

ok, thanks

#### Mario Carneiro (Mar 13 2019 at 18:58):

linear_order_of_STO'

Last updated: May 11 2021 at 13:22 UTC