FPIL section 10.3: termination_by fails with "Too many ..."

Stream: new members

[Josha Dekker]

Hi, I'm working through section 10.3 of FPIL and was trying to run the code for myself, but I get the same error for the first two examples from that section:

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 findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Nat × α) :=
  if h : i < arr.size then
    let x := arr[i]
    if p x then
      some (i, x)
    else findHelper arr p (i + 1)
  else none
termination_by -- Too many extra parameters bound; the function definition only has 0 extra parameters.
  findHelper arr p i => arr.size - i

Any clue? these are just copy-pasted from https://lean-lang.org/functional_programming_in_lean/programs-proofs/arrays-termination.html.

[Ruben Van de Velde]

This changed in lean recently. I think you can just drop the name of the definition in the termination by clause

[Josha Dekker]

Thanks! dropping the entire LHS worked for me:

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

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

[Josha Dekker]

I'll file an issue as well on the GitHub