classical and classical! tactics

def Mathlib.Tactic.classical! : Lean.ParserDescr

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)

def Mathlib.Tactic.tacticClassical_ : Lean.ParserDescr

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.