# Documentation

Mathlib.Tactic.Classical

# classical and classical! tactics #

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.

Instances For

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.

Instances For