From 44e889bd5286ed529306ace1397adcc758daabec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 27 Oct 2022 07:48:30 -0700
Subject: [PATCH] chore: avoid runtime bounds check

---
 src/Lean/Environment.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index b7a265fdd5..d7cf0c37e6 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -646,8 +646,8 @@ def writeModule (env : Environment) (fname : System.FilePath) : IO Unit := do
   saveModuleData fname env.mainModule (← mkModuleData env)
 
 private partial def getEntriesFor (mod : ModuleData) (extId : Name) (i : Nat) : Array EnvExtensionEntry :=
-  if i < mod.entries.size then
-    let curr := mod.entries.get! i;
+  if h : i < mod.entries.size then
+    let curr := mod.entries[i]
     if curr.1 == extId then curr.2 else getEntriesFor mod extId (i+1)
   else
     #[]