Updating local context in tactics

Stream: lean4

[Siddhartha Gadgil]

I was trying to add a let declaration from within a tactic. Below I create a new local context, but then just discard it (as expected it does not work as a let). Can someone help me with what is the missing statement to update the local context (or am I getting the idiom wrong). I have been trying to copy the code of the introtactic but could not see where the updating takes place.

syntax (name:= dupllet) "assign" ident "::" term "as" term : tactic
@[tactic dupllet] def assignImpl : Tactic :=
  fun stx =>
    match stx with
    | `(tactic|assign $n:ident :: $t as  $i) =>
      do
        let fvarId ← mkFreshFVarId
        let name ← n.getId
        let typ ← liftM (Elab.Term.elabTerm t none true true)
        let value ← liftM (Elab.Term.elabTerm i (some typ) true true)
        let lctx ← getLCtx
        let lctx ← lctx.mkLetDecl fvarId name typ value
        let fvar   := mkFVar fvarId
        return ()
    | _ => Elab.throwIllFormedSyntax

[Siddhartha Gadgil]

I tried an alternative approach, which also did not work, i.e., the new let statement did not appear.

syntax (name:= dupllet) "assign" ident "::" term "as" term : tactic
@[tactic dupllet] def assignImpl : Tactic :=
  fun stx =>
    match stx with
    | `(tactic|assign $n:ident :: $t as  $i) =>
      do
        let fvarId ← mkFreshFVarId
        let name ← n.getId
        let typ ← liftM (Elab.Term.elabTerm t none true true)
        let value ← liftM (Elab.Term.elabTerm i (some typ) true true)
        let mvar ← getMainGoal
        withMVarContext mvar do
          let mvar2 ← mkFreshExprMVar (← getMVarType mvar)
          let mvarId2 := mvar2.mvarId!
          replaceMainGoal [mvarId2]
          withLetDecl  name  typ value $ fun x =>
            do
            assignExprMVar mvar (← mkLetFVars #[x] mvar2)
            return ()
    | _ => Elab.throwIllFormedSyntax

[Siddhartha Gadgil]

Update: I managed to make a tactic with the correct result using apply and intro at the Meta level and liftMetaTactic.

For the sake of my understanding, I would be grateful for tips on doing this in a more self-contained way.

Thanks.