classical tactic

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.

def Batteries.Tactic.tacticClassical! : Lean.ParserDescr

classical! has been removed; use classical instead

Equations

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

def Batteries.Tactic.tacticClassical_ : Lean.ParserDescr

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.