Building let expressions

Stream: lean4

[Siddhartha Gadgil]

I have been experimenting with building expressions and most are working very nicely with the helpers. However I am struggling with let expressions. The following is wrong code

syntax (name := minlet) "minlet!" : term

@[termElab minlet] def minletImpl : TermElab :=
  fun stx expectedType? =>
  let n := Name.mkSimple "n"
  let z := Lean.mkConst `Nat.zero
  let ty := Lean.mkConst `Nat
  withLetDecl n ty z fun x => do
    let e <- mkLet n (mkConst `Nat) z (mkFVar n)
    return e

#check minlet!

The command #check minlet! gives "unknown free variable n". I tried a few variants like using mkConst n and using x but clearly I am making a more basic mistake (I also tried skipping the withLetDecl part).

Can someone help me by saying what is the correct way to refer to the name in the body of the let declaration?
Thanks.

[Sebastian Ullrich]

Note that (this) mkLet is not monadic, so that's a good hint that it is not supposed to be used together with withLetDecl. The correct function, from the same Lean.Meta namespace as withLetDecl, is

    let e <- mkLetFVars #[x] x

[Siddhartha Gadgil]

Thanks a lot. That fixed the minimal case. I will try to fix the real case too (needs nested do's).