chore: remove unnecessary private Inhabited instance (#5846)

Since `partial` inhabitation is stronger in #5821, this private instance is no longer needed.
leanprover · Oct 25, 2024 · 4068cf0 · 4068cf0
1 parent abe6d5b
commit 4068cf0
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
@@ -767,9 +767,6 @@ where
 
 namespace Trie
 
--- `Inhabited` instance to allow `partial` definitions below.
-private local instance [Monad m] : Inhabited (σ → β → m σ) := ⟨fun s _ => pure s⟩
-
 /--
 Monadically fold the keys and values stored in a `Trie`.
 -/