recursion in match expressions

Stream: new members

[Nick Yu]

I just started learning Lean but I have a bit of a noob-ish question, I'm not sure if this is the right place to ask but,

In the second example in this snippet:

def example₁ : ℕ -> bool
| 0 := tt
| 1 := ff
| (n + 2) := example₁ n

def example₂ : ℕ -> bool := λn,
match n with
| 0 := tt
| 1 := ff
| (n + 2) := example₂ n
end

lean is complaining that the identifier example₂ does not exist.
I was wondering what the difference is between the match syntax in example 1 and the match expression in example 2 that disallows the recursive definition.

[Arthur Paulino]

Eric Wieser said:

Note that in lean3 the recursion only works if you use the equation compiler

This is improved in Lean 4, but Lean 3 relies on your first way of writing for defining recursive functions

[Eric Wieser]

Don't do this, but this works:

def example₂ : ℕ -> bool := λn,
match n with
| 0 := tt
| 1 := ff
| (n + 2) := by exact _match n
end

[Arthur Paulino]

Just to illustrate, these compile just fine in Lean 4:

def example₂ : Nat → Bool := fun n =>
  match n with
  | 0     => true
  | 1     => false
  | n + 2 => example₂ n

def example₂' (n : Nat) : Bool :=
  match n with
  | 0     => true
  | 1     => false
  | n + 2 => example₂' n