Did I write something wrong?

Stream: lean4

[👀？]

def shortest_aux (ps : List (Nat × Nat × Nat)) (o : Nat) (g : Nat) (ctx : List Nat) (l : Nat)
  : Nat × List (Nat × Nat × Nat) :=
  match ps with
  | [] => (0, [])
  | p :: ps' =>
    let (o', l', g') := p
    if o' = o ∧ g' = g then (l+l', [p])
    else if o' = o ∧ ctx.notElem g' then
      match shortest_aux ps g' g (g' :: ctx) (l+l') with
      | (0, []) => (0, [])
      | (l', es') => (l+l', p :: es')
    else shortest_aux ps' o g ctx l

fail to show termination for
  shortest_aux
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    shortest_aux ps g' g (g' :: ctx) (l + l')

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    shortest_aux ps g' g (g' :: ctx) (l + l')

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    shortest_aux ps g' g (g' :: ctx) (l + l')

argument #4 was not used for structural recursion
  failed to eliminate recursive application
    shortest_aux ps g' g (g' :: ctx) (l + l')

argument #5 was not used for structural recursion
  failed to eliminate recursive application
    shortest_aux ps g' g (g' :: ctx) (l + l')

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relationLean 4

[Henrik Böving]

Its not necessarily wrong, lean just cannot do the termination proof automatically so you have to. There is documentation in theorem proving in Lean on how to do that

[👀？]

How do I write a termination proof?

[Alex J. Best]

https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction explains some examples of this