From 40e97bd5666803b28936316b59c6abd96d9a4e73 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 29 Sep 2024 15:53:12 +1000
Subject: [PATCH] chore: upstream Subarray.empty (#5516)

---
 src/Init/Data/Array/Subarray.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 53f62af865..efc255868c 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -59,6 +59,22 @@ def popFront (s : Subarray α) : Subarray α :=
   else
     s
 
+/--
+The empty subarray.
+-/
+protected def empty : Subarray α where
+  array := #[]
+  start := 0
+  stop := 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
+
+instance : EmptyCollection (Subarray α) :=
+  ⟨Subarray.empty⟩
+
+instance : Inhabited (Subarray α) :=
+  ⟨{}⟩
+
 @[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   let sz := USize.ofNat s.stop
   let rec @[specialize] loop (i : USize) (b : β) : m β := do