def
Batteries.Tactic.classical
{m : Type → Type}
{α : Type}
[Monad m]
[Lean.MonadEnv m]
[MonadFinally m]
[MonadLiftT Lean.MetaM m]
(t : m α)
:

m α

`classical t`

runs `t`

in a scope where `Classical.propDecidable`

is a low priority
local instance.

## Equations

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

## Instances For

`classical!`

has been removed; use `classical`

instead

## Equations

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

## Instances For

`classical tacs`

runs `tacs`

in a scope where `Classical.propDecidable`

is a low priority
local 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.