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.

Equations
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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For