From 64258d0dd717b8d9caae36d00912f89feb0feb99 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 13 Feb 2026 16:32:20 +0000
Subject: [PATCH] feat: `Thunk` is inhabited

---
 src/Init/Core.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 315ef6868bfd..6b538b773403 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -171,6 +171,8 @@ instance thunkCoe : CoeTail α (Thunk α) where
   -- Since coercions are expanded eagerly, `a` is evaluated lazily.
   coe a := ⟨fun _ => a⟩
 
+instance [Inhabited α] : Inhabited (Thunk α) := ⟨.pure default⟩
+
 /-- A variation on `Eq.ndrec` with the equality argument first. -/
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h