def
Lean.Elab.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.
Instances For
Equations
- One or more equations did not get rendered due to their size.