Server crashes on index out of bounds

Stream: lean4

[Alex Sweeney]

I'm working on section 4.4 (Arrays and Indexing) of the Functional Programming in Lean book. The book says that Lean should throw a compile error, but something is clearly extra broken. Is this issue my fault or Lean's?

Here's the code in text

-- 4.4 Arrays and Indexing

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop :=
  i ≤ xs.tail.length

def NonEmptyList.get (xs : NonEmptyList α) (i : Nat) (ok : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n + 1 => xs.tail[n]

instance : GetElem (NonEmptyList α) Nat α NonEmptyList.inBounds where
  getElem := NonEmptyList.get

#eval idahoSpiders[0]
-- "Banded Garden Spider"

#eval idahoSpiders[5]
-- Server crashes

image.png

[Damiano Testa]

This seems similar to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/LSP.20crash.

[Kyle Miller]

@Alex Sweeney This should be a workaround so that you can see an error without crashing Lean:

def x := idahoSpiders[5]