let telescope and have

Stream: lean4

[Tomas Skrivan]

Can someone explain me this behavior?

run_meta
  let e := q(have a := 1
             have b := 2
             a + b + 10)
  let e' ← letTelescope e fun xs b =>
    mkLetFVars xs b
  logInfo e'  -- fun a b => a + b + 10

Why do those have bindings get turned into a lambda? Is this intended behavior? I find this really surprising behavior.

[Henrik Böving]

I can't tell you why but you can unset the generalize flag on mkLetFVars to not make it do that

[Tomas Skrivan]

Hmm strange, there is also a flat on letTelescope to prevent that from happening but all have gets turned into let, but I don't care too much so it works for me.