how to fill metavariables when compiling function in command

Stream: lean4

[Michael Jam]

I'm trying to compile a function after manually constructing its syntax, but I run into meta variables problems.
As a simple example, let's say I want to generate a function of type Nat that returns 42.
In regular lean I can just do def f : Nat := 42 but here I'm getting an (kernel) declaration has metavariables error.
How can I fix it?

import Lean
open Lean Elab Command Term Meta

elab "cmd" : command => do
  let name := `f
  let type <- liftTermElabM .none <| flip elabTerm .none <| <- `(Nat)
  let val <- liftTermElabM name <| flip elabTerm (.some type) <| <- `(42)
  let decl := Declaration.defnDecl <| mkDefinitionValEx name [] type val .opaque .safe
  match (<- getEnv).addAndCompile {} decl with
  | .error e =>
    match e with
    | KernelException.declHasMVars env name expr =>
      IO.println <| "declHasMVars"
      IO.println <| "name: " ++ name.toString
      IO.println <| "expr: " ++ expr.dbgToString
    | _ => return ()
    throwError (e.toMessageData {})
  | .ok env => setEnv env
cmd
#print f

Thanks for suggestions/solutions

[Siddhartha Gadgil]

There is a function assignExprMVar which you can use.

[Siddhartha Gadgil]

Such as in the example assignExprMVar mvarId2 (mkApp (mkConst ``Nat.succ) mvar)

[Henrik Böving]

But the issue here is that they don't even know where the meta variables are no? At least I certainly cannot see any being introduced manually.

[Michael Jam]

I think instantiateMVars is what I need

[Michael Jam]

I replaced the let val line with let val <- liftCoreM <| MetaM.run' <| return (<- instantiateMVars (<- (TermElabM.run' <| withDeclName name <| flip elabTerm (.some type) <| <- `(42)))) and it works (I know the style is ugly).