# `classical` tactic #

source
def Lean.Elab.Tactic.classical {m : Type → Type} {α : Type} [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT 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

source
def Lean.Elab.Tactic.evalClassical :
Tactic
Equations

- Lean.Elab.Tactic.evalClassical stx = Lean.Elab.Tactic.classical (Lean.Elab.withSaveInfoContext (Lean.Elab.Term.withNarrowedArgTacticReuse 1 Lean.Elab.Tactic.evalTactic stx))

Instances For