Argument for tactic as expression

Stream: lean4

[Siddhartha Gadgil]

I am trying to pass an argument to a tactic. I tried to use Elab.Tactic.elabTerm to parse the syntax of the expression. This works fine for local expressions, but not for let declarations. Is there some method that elaborates using the local context?

Thanks.