How to apply `whnf ` to hypotheses in a tactic?

Stream: new members

[Zihao Zhang]

How to correct the line that has been commented out?

import Mathlib

open Lean Elab IO Meta Tactic
elab "my_tool" :tactic => do
    let g ← getMainGoal
    let g_lctx ← getLCtx
    for ldecl in g_lctx do
        --evalTactic (← `(tactic| whnf at $(ldecl)))
    evalTactic (← `(tactic| whnf))