have h : x = x via tactic

Stream: lean4

[Ian Benway]

Hi! I'm learning metaprogramming in Lean 4. I've managed to write something that allows me to add a hypothesis to the local context:

private def defineV (nm : Name) (tp : Expr) (tme : Expr) : TacticM Unit := do
  liftMetaTactic1 fun mvarId => do
    let h2 ← (define mvarId nm tp tme)
    let (h, h2) ← intro1P h2
    withMVarContext h2 do
      return h2

so that in my elaborator, I can have

defineV nm tp tme

add nm : tp := tme to the context.
However now, I want to add something like h : x = x to the context. This might be a silly question, I'm a bit new, but if I have x : Expr as an expression already, is there a way to get an expression of x=x? Or rather in general, how might I add something like this? (Once I get that, I think I can apply applyRefl, right?)

[Siddhartha Gadgil]

To get the expression x = x you can use use mkEq