Elaborating values in expresions

Stream: new members

[Fox Thomson]

I would like to make a function that takes an input a and returns an expression of the form `(∃ x, a = x). How would I get this elaborated so I can use it in a tactic. Currently I have

meta def ex {α : Type} (a : α) : expr :=
  `(∃ x, a = x)

[Mario Carneiro]

This should almost work:

meta def ex (a : expr) : expr :=
  `(∃ x, %%a = x)

but I think there is a free universe variable

[Mario Carneiro]

alternatively:

meta def ex (a : expr) : tactic expr :=
to_expr ``(∃ x, %%a = x)

[Fox Thomson]

What is the to_expr function?

[Mario Carneiro]

tactic.to_expr

[Mario Carneiro]

You might want to see Rob's metaprogramming tutorial if you haven't done it before

[Fox Thomson]

Thank you