Allow holes in lemma statement

Stream: lean4

[Bolton Bailey]

I'd like to have a hole in my lemma statement so that I don't have to calculate beforehand what the result of the lemma will be. Interestingly, this seems to work perfectly but also throws an error. How do I get the error to go away? Is this a bug that it's an error in the first place?

import Mathlib.LinearAlgebra.Lagrange

lemma foo : 2 + 2 = _ := by -- when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
  norm_num
  rfl

lemma bar (a : ℕ) : 2 + 2 + a = a + 4 := by
  rw [foo, add_comm] -- Works fine, state shows 4 + a = a + 4 after foo

[Mario Carneiro]

you can't do this for lemma, but if you use def you can omit the return type entirely and put it inside the body of the definition:

def foo := show 2 + 2 = _ by
  norm_num
  rfl

[Mario Carneiro]

this is a deliberate restriction, to make it easier to read theorem statements, avoid surprising changes to the theorem statement caused by tactics in the body, and also (in theory) to allow theorem bodies to be processed in parallel