termination_by usage changed

[JADekker]

In sections 10.3 and onward, users are introduced to termination_by. I think the phrasing of this has changed recently in Lean, for example the definition of arrayMapHelper doesn't work for me, but it does work upon removing some aspects:

Doesn't work:

def arrayMapHelper (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if inBounds : i < arr.size then
    arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
  else soFar
termination_by -- Too many extra parameters bound; the function definition only has 0 extra parameters.
  arrayMapHelper _ arr _ i _ => arr.size - i

def arrayMapHelper2 (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if inBounds : i < arr.size then
    arrayMapHelper2 f arr (soFar.push (f arr[i])) (i + 1)
  else soFar
termination_by _ arr _ i _ => arr.size - i -- fails with same error

Does work:

def arrayMapHelper3 (f : α → β) (arr : Array α) (soFar : Array β) (i : Nat) : Array β :=
  if inBounds : i < arr.size then
    arrayMapHelper3 f arr (soFar.push (f arr[i])) (i + 1)
  else soFar
termination_by arr.size - i -- works