Documentation

Batteries.Tactic.Classical

classical tactic #

def Batteries.Tactic.classical {m : TypeType} {α : 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.
Instances For

    classical! has been removed; use classical instead

    Equations
    Instances For

      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.
      Instances For