## Stream: general

### Topic: prop_decidable breaks dec_trivial?

#### 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?

#### Patrick Massot (Jul 26 2018 at 15:32):

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

Works! Thanks!

#### Kevin Buzzard (Jul 26 2018 at 15:33):

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

#### Patrick Massot (Jul 26 2018 at 15:33):

We really need that tips_and_tricks.md in mathlib docs

#### 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"

#### Patrick Massot (Jul 26 2018 at 15:43):

Good question!

Last updated: May 13 2021 at 21:12 UTC