List.getLast! making Lean4 panic

Stream: new members

[Vivek Rajesh Joshi]

I've got this code that requires extracting the index of the last entry of a row that equals 1:

def is_rrf_row (ri : List Rat) : Bool×Nat :=
  let should_0 := ri.after (fun x => ((ri.indexOf x) == (ri.indexesOf 1).getLast!))
  if should_0.all (fun x => x==0) then (True,(ri.indexesOf 1).getLast!)
  else (False,0)

It works, but it keeps giving this warning in a dialogue box at the bottom right of my screen:
"Lean server printed an error:
PANIC at List.getLast! Init.Data.List.BasicAux:63:13: empty list
PANIC at List.getLast! Init.Data.List.BasicAux:63:13: empty list"
Can I ignore it, or should I try to modify my code and get rid of the warning?

[Mario Carneiro]

you are trying to get the last element of an empty list, you should probably rewrite the code to not do this

[Mario Carneiro]

the standard position is that panics are always a bug in the code

[Mario Carneiro]

the index of the last entry of a row that equals 1

Lean is asking you to consider the question "what if there is no such entry?"

[Mario Carneiro]

and the fact you are getting this panic indicates that the answer is not "it's fine because the code will never be called in that case"

[Vivek Rajesh Joshi]

Thanks, fixed it now