From ee0735760a47bc5884433c67fbef5bfa777cab0f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jul 2022 17:38:59 -0700
Subject: [PATCH] =?UTF-8?q?feat:=20add=20`instance=20:=20GetElem=20(List?=
 =?UTF-8?q?=20=CE=B1)=20Nat=20=CE=B1=20fun=20as=20i=20=3D>=20i=20<=20as.le?=
 =?UTF-8?q?ngth`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Init/Data/List/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index e5fa024922..dd012eeed4 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -14,6 +14,9 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]