From 518a1357770464d87b123f8fa3d976189018d769 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Date: Thu, 19 Mar 2026 21:58:46 +0000
Subject: [PATCH] feat: `Thunk` is inhabited (#12469)

This PR adds the `Inhabited` instance for `Thunk`.

We need this in batteries to call `PersistentEnvExtension.getState` on a
state that is wrapped in a `Thunk`, see
https://github.com/leanprover-community/batteries/pull/1667/changes.
---
 src/Init/Core.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 67ba3a75a1..21c3f2d92f 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -172,6 +172,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