Array Index in eval

Stream: lean4

[Henrik Böving]

#mwe:

def test : Array String := #["a", "b", "c"]
#eval test[2] -- works
#eval test[3] -- crashes my LSP

I would expect Lean to refuse the second line based on the fact that it cannot proof 3 is within bounds. If i were to use this syntax in a function it also does this precise behaviour. It also does not crash if I use ! or ? array access syntax like so:

def foo : String := test[3]

What is special about #eval here? shouldn't it elaborate the term in the same way it would be in the position of a definition body.

[Gabriel Ebner]

lean4#1697