`classical`

and `classical!`

tactics #

`classical!`

adds a proof of `Classical.propDecidable`

as a local variable, which makes it
available for instance search and effectively makes all propositions decidable.

```
noncomputable def foo : Bool := by
classical!
have := ∀ p, decide p -- uses the classical instance
exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
```

Consider using `classical`

instead if you want to use the decidable instance when available.

## Equations

- Mathlib.Tactic.classical! = Lean.ParserDescr.node `Mathlib.Tactic.classical! 1024 (Lean.ParserDescr.nonReservedSymbol "classical!" false)

`classical tacs`

runs `tacs`

in a scope where `Classical.propDecidable`

is a low priority
local instance. It differs from `classical!`

in that `classical!`

uses a local variable,
which has high priority:

```
noncomputable def foo : Bool := by
classical!
have := ∀ p, decide p -- uses the classical instance
exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
def bar : Bool := by
classical
have := ∀ p, decide p -- uses the classical instance
exact decide (0 < 1) -- uses the decidable instance
```

Note that (unlike lean 3) `classical`

is a scoping tactic - it adds the instance only within the
scope of the tactic.

## Equations

- One or more equations did not get rendered due to their size.