Inserting `Expr` into command syntax

Stream: metaprogramming / tactics

[Daniil Kisel]

I'm trying to insert a runtime value into command syntax:

run_cmd do
  let y ← liftTermElabM <| Term.exprToSyntax <| ToExpr.toExpr 0
  elabCommand (← `(def x : Nat := $y))

But it shows an error:

don't know how to synthesize placeholder
context:
case m
⊢ Nat

Is it possible to insert an Expr into Syntax that goes to elabCommand?