classical tactic

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.

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))