From bb2de82cb6f3f7d6437e7ee5f104bdcf523c079b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Mar 2022 17:47:40 -0800
Subject: [PATCH] chore: update stage0

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

diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean
index c14a7d5cfb..04d219d9e2 100644
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@@ -42,6 +42,9 @@ attribute [extern "lean_mk_thunk"] Thunk.mk
 @[inline] protected def Thunk.bind (x : Thunk α) (f : α → Thunk β) : Thunk β :=
   ⟨fun _ => (f x.get).get⟩
 
+@[simp] theorem Thunk.sizeOf_eq [SizeOf α] (a : Thunk α) : sizeOf a = 1 + sizeOf a.get := by
+   cases a; rfl
+
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h