eval expr in MetaM

Stream: lean4

[James Gallicchio]

first some #xy: I want to write a macro that is called as

getStatusCodes! [
  (a,b,c,d),
  (e,f,g,h),
...
]

because I assumed it would be easier to just use term parser instead of making a custom syntax for this. But I need the (evaluated) value within the macro implementation. Is there a function to run a term or elaborated expr?

I see #eval just adds a new declaration to the environment, calls evalConst, and then resets the environment. Is there a function that already does this somewhere in core/std?

[James Gallicchio]

and if I should just make a custom syntax category, then I will do that :p

[James Gallicchio]

(this would also be nice to have as an abstraction so that the evalConst unsafeness can be hidden)

[Joachim Breitner]

https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Eval.html#Lean.Meta.evalExpr maybe?

[James Gallicchio]

ooh that does look like the right signature

[James Gallicchio]

don't love that it's unsafe
EDIT: termUnsafe saves the day :)