Debugging metaprogramming in TermElabM

Stream: metaprogramming / tactics

[Segev Elazar Mittelman]

How do I evaluate the result of a TermElabM to do unit testing of my metaprogramming?

For instance, how do I get this to work?

#eval (do pure $ Lean.Elab.Term.elabType (← constructorExprToTSyntaxTerm (.Ctor ``String [])))

[Aaron Liu]

if you have a t : TermElabM Expr you can use by_elab t

[Segev Elazar Mittelman]

Thank you!