From d8e0fa425b3225fc0c35c07247ecb11b49bb00ed Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 20 Sep 2024 01:07:02 -0500
Subject: [PATCH] =?UTF-8?q?feat:=20instance=20for=20`Inhabited=20(TacticM?=
 =?UTF-8?q?=20=CE=B1)`=20(#5401)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Provide an instance `Inhabited (TacticM α)`, even when `α` is not known
to be inhabited.

The default value is just the default value of `TermElabM α`, which
already has a similar instance.
---
 src/Lean/Elab/Tactic/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 505ca4cfff..f58c7820cd 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -49,6 +49,9 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
+instance : Inhabited (TacticM α) where
+  default := fun _ _ => default
+
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals