chore: monadic implementation of classical (#714)

Co-authored-by: Mario Carneiro <[email protected]>

Std/Tactic/Classical.lean

@@ -8,7 +8,7 @@ import Lean.Elab.ElabRules
 /-! # `classical` and `classical!` tactics -/
 
 namespace Std.Tactic
-open Lean Meta
+open Lean Meta Elab.Tactic
 
 /--
 `classical!` adds a proof of `Classical.propDecidable` as a local variable, which makes it
@@ -24,6 +24,19 @@ Consider using `classical` instead if you want to use the decidable instance whe
 macro (name := classical!) "classical!" : tactic =>
   `(tactic| have em := Classical.propDecidable)
 
+/--
+`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
+local instance.
+-/
+def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
+    m α := do
+  modifyEnv Meta.instanceExtension.pushScope
+  Meta.addInstance ``Classical.propDecidable .local 10
+  try
+    t
+  finally
+    modifyEnv Meta.instanceExtension.popScope
+
 /--
 `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,
@@ -45,7 +58,4 @@ scope of the tactic.
 -- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when
 -- the `classical` does not scope over the rest of the block.
 elab "classical" tacs:ppDedent(tacticSeq) : tactic => do
-  modifyEnv Meta.instanceExtension.pushScope
-  Meta.addInstance ``Classical.propDecidable .local 10
-  try Elab.Tactic.evalTactic tacs
-  finally modifyEnv Meta.instanceExtension.popScope
+  classical <| Elab.Tactic.evalTactic tacs