Zulip Chat Archive

Stream: general

Topic: prop_decidable breaks dec_trivial?


view this post on Zulip Kevin Buzzard (Jul 26 2018 at 15:24):

local attribute [instance] classical.prop_decidable
example : (-1:)  (0:) := dec_trivial -- fails
/-
exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true (-1 ≠ 0)
state:
⊢ as_true (-1 ≠ 0)
-/

In practice this is in the middle of a big file which needs decidable props but occasionally also needs simple calculations like this. Is this expected behaviour?

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:32):

Did you try local attribute [instance, priority 0] classical.prop_decidable?

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 15:33):

Works! Thanks!

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 15:33):

What's happening here? Oh -- we have two instances

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:33):

We really need that tips_and_tricks.md in mathlib docs

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 15:39):

I sometimes wonder why we can't solve diamond issues using priorities. "now we have two instances of topological_space (X x Y) and they're equal but not defeq so we have rw problems" -- "well just make the one you want a higher priority"

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:43):

Good question!


Last updated: May 13 2021 at 21:12 UTC