## Stream: new members

### Topic: dec_trivial in classical

#### Kenny Lau (Apr 12 2020 at 08:34):

how to make dec_trivial work when I have an instance of all propositions decidable? MWE:

import tactic

example : nat.coprime 127 128 :=
by classical; exact dec_trivial


#### Kevin Buzzard (Apr 12 2020 at 08:35):

oh wow I thought this stuff had been solved.

#### Kevin Buzzard (Apr 12 2020 at 08:35):

import tactic

/-! -/
open_locale classical

example : nat.coprime 127 128 :=
by exact dec_trivial


Oh I see. This works

#### Kevin Buzzard (Apr 12 2020 at 08:36):

The classical tactic adds _inst : Π (a : Prop), decidable a to the type class inference system but ideally it would add it with priority 10

#### Mario Carneiro (Apr 12 2020 at 08:36):

classical puts decidability in your context, and I think that gets maximum precedence

#### Kevin Buzzard (Apr 12 2020 at 08:38):

Could classical instead do what open_locale classical does?

#### Mario Carneiro (Apr 12 2020 at 08:39):

I don't think so? Changing declarations in the environment in the middle of a proof is kind of weird

#### Mario Carneiro (Apr 12 2020 at 08:40):

Certainly it can't do everything that open_locale can do because open_locale runs in the parser monad and hence has the ability to inject commands into the file that tactics can't do

#### Mario Carneiro (Apr 12 2020 at 08:40):

but maybe open_locale classical just sets some precedences and those might be doable

Last updated: May 10 2021 at 00:31 UTC