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
Simon Hudon (Apr 15 2020 at 15:28):
Can you show your code?
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
Reid Barton (Apr 15 2020 at 15:43):
I don't know.
Simon Hudon (Apr 15 2020 at 15:45):
If we compare with
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