let rec puzzle

Stream: lean4

[Eric Rodriguez]

theorem test :
  let rec f : Nat → Nat :=
    fun n => match n with | n => n
  f 0 = 0 := by
  done

What's the goal state?

(fun f => f 0 = 0) ?m.5. This is because let recs are, in theory, allowed to recurse with test itself. (doesn't seem to be in practice - I read this in one of Mario's posts so not sure?) But I think this should give an error message instead of a nonsense goal.

[Mario Carneiro]

Ah, you can't recurse with the main definition inside the type of the definition itself

[Mario Carneiro]

although I'm not sure the elaborator knows this

[Mario Carneiro]

i.e. this doesn't work

partial def foo : foo := foo

[Joachim Breitner]

Also this doesn’t work

foo := bar
  where
    myType := Nat
    bar : myType := 42

which is unfortunate, at least once I wanted to put a large monad stack into a where M :=.

[Kyle Miller]

There are some complexities here, but it would be interesting if where blocks required explicit lets and let recs before each definition. Or at least required an explicit rec in front of a where definition if it was meant to be a let rec.

[Kyle Miller]

Like

def f := bar
where
  myType := Nat
  rec bar (n : myType) : myType := match n with | 0 => 0 | n + 1 => bar n