How can I use expr inside syntax `(..)?

Stream: lean4

[Juneyoung Lee]

Hi all, I have a naive question about metaprogramming.
Given some x:Lean.Expr, how can I use it inside syntax e.g., (tactic| .. x ..)?

[Marcus Rossel]

docs4#Lean.Expr.toSyntax

[Juneyoung Lee]

Oops, I mistakenly posted this at the general stream. Moving this thread to a different stream (lean4) is disabled, however. :/

[Juneyoung Lee]

Thanks!

[Notification Bot]

This topic was moved here from #general > How can I use expr inside syntax `(..)? by Kyle Miller.