## Stream: general

### Topic: classical tactic and linear orders

#### Patrick Massot (Apr 15 2020 at 15:16):

Is it a bug in the classical tactic that Lean still complains it can't find a decidable_linear_order instance even after calling classical?

#### Sebastien Gouezel (Apr 15 2020 at 15:31):

The standard way is letI := classical.DLO γ.

#### Patrick Massot (Apr 15 2020 at 15:32):

Yes, I know the standard way, but I thought classical would take care of that.

#### Simon Hudon (Apr 15 2020 at 15:38):

classical only adds decidable_prop to the local set of instances.

#### Mario Carneiro (Apr 15 2020 at 15:38):

Unfortunately not; we could have an instance that derives DLO from LO but it would loop

#### Reid Barton (Apr 15 2020 at 15:39):

The problem is DLO extends LO

#### Simon Hudon (Apr 15 2020 at 15:40):

would it be better if LO was an argument of DLO?

#### Simon Hudon (Apr 15 2020 at 15:41):

I mean in general, with the rest of the library

I don't know.

#### Simon Hudon (Apr 15 2020 at 15:45):

If we compare with is_lawful_functor, DLO doesn't add propositional fields but it is a subsingleton

#### Mario Carneiro (Apr 15 2020 at 15:57):

I suppose that since classical is a tactic, it can do some intelligent things here. In particular, it can look for linear_order foo things in the local context and add letI := classical.DLO foo as necessary

#### Simon Hudon (Apr 15 2020 at 15:59):

That's true, that would be simple enough.

Last updated: May 08 2021 at 04:14 UTC