Panic in Array

Stream: lean4

[Moritz Firsching]

I'm trying to understand the following code:
https://github.com/leanprover/lean4/blob/510bc47cc366e7d231c62c31f7ec1cbbacda9e6d/src/Init/Prelude.lean#L2528-L2531

/-- Access an element from an array, or panic if the index is out of bounds. -/
@[extern "lean_array_get"]
def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
  Array.getD a i default

In get! for List, I can see the how the panic is happening clearly:
https://github.com/leanprover/lean4/blob/510bc47cc366e7d231c62c31f7ec1cbbacda9e6d/src/Init/Data/List/BasicAux.lean#L17-L20

def get! [Inhabited α] : List α → Nat → α
  | a::_,  0   => a
  | _::as, n+1 => get! as n
  | _,     _   => panic! "invalid index"

But how is a panic obtained for the Array? Will it not just return default?

[François G. Dorais]

The C implementation of "lean_array_get" does call "lean_array_get_panic" when the index is out of bounds. The reference implementation you see is compatible with that since panic! is basically a sugar-coated function that returns default.

[Ruben Van de Velde]

This is the real code: https://github.com/leanprover/lean4/blob/510bc47cc366e7d231c62c31f7ec1cbbacda9e6d/src/include/lean/lean.h#L741