From 167e0ab301690e44e1a7e0dc05e4b6ee70c968cf Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 18 Feb 2025 17:14:14 +1100
Subject: [PATCH] chore: add Array.getInternal, also @[extern]

---
 src/Init/Prelude.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index f94d8057b8..1d5c088376 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2676,6 +2676,20 @@ arrays.
 def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
   a.toList.get ⟨i, h⟩
 
+/--
+Use the indexing notation `a[i]` instead.
+
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays.
+-/
+@[extern "lean_array_fget"]
+def Array.getInternal {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+  a.toList.get ⟨i, h⟩
+
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
   dite (LT.lt i a.size) (fun h => a.get i h) (fun _ => v₀)
@@ -2689,6 +2703,15 @@ Access an element from an array, or panic if the index is out of bounds.
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
+@[extern "lean_array_get"]
+def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+  Array.getD a i default
+
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.