recursive functions and `variable`

Stream: lean4

[James Sully]

Is it expected that tri' doesn't compile?

def tri (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | m + 1 => n + tri m

section
variable (n : Nat)

def tri' : Nat :=
  match n with
  | 0 => 0
  | m + 1 => n + tri' m

end

[Kyle Miller]

Yes, you can only do recursion on variables in the function's parameter list.

(A recent thread)

[James Sully]

Thanks! I guess my intuition that variable just adds to the parameter list of any definition that refers to it is subtly wrong

[Kyle Miller]

Not an explanation for why it works this way, but during elaboration these parameters are added before your tri' starts to be elaborated, and during elaboration a local function tri' is added (later, any calls to tri' will be "compiled out"). It makes some sense that this local tri' wouldn't be responsible for pre-existing variables.

[James Sully]

I can't quite follow this sorry

a local function tri' is added

• what does "local" mean in this context?
• added to what?
• isn't tri' already there?

[Kyle Miller]

Added to the local context.

The tri' function doesn't exist globally until after the whole definition is elaborated and processed. Until then, there's a secret tri' function in the local context that you're referring to. (It's marked in such a way that you can't see it in the Infoview.)