[Typo] Section 8.5 recursion on wrong var in Nat.plusR rhs

[mars0i]

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

The recursion doesn't reduce the size of either Nat and generates a "Failed to show termination" error. I believe the last line should be

  | n, k + 1 => plusRinbook (n + 1) k 

Full error text:

▶ 8:5-8:14: error:
fail to show termination for
  Nat.plusR
with errors
failed to infer structural recursion:
Cannot use parameter #1:
  failed to eliminate recursive application
    n.plusR (k + 1)
Cannot use parameter #2:
  failed to eliminate recursive application
    n.plusR (k + 1)

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            x1 x2
1) 10:16-31  =  =
Please use `termination_by` to specify a decreasing measure.

[david-christiansen]

Thanks!

[mars0i]

My report is incorrect. It's an embarrassing rookie mistake. I interpreted the code in FPIL,

def Nat.plusR : Nat -> Nat -> Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

as

def Nat.plusR : Nat -> Nat -> Nat
  | n, 0 => n
  | n, k + 1 => plusR n (k + 1)

which doesn't terminate, rather than

def Nat.plusR : Nat -> Nat -> Nat
  | n, 0 => n
  | n, k + 1 => (plusR n k) + 1

which does. I added the parentheses around k + 1 in my code, and then didn't copy the parentheses into this report. The original FPIL definition, without added parentheses, doesn't generate a termination error in Lean 4.13.0-rc3.