Zulip Chat Archive

Stream: new members

Topic: Elaborating values in expresions


Fox Thomson (Sep 04 2020 at 10:34):

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 (Sep 04 2020 at 10:36):

This should almost work:

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

but I think there is a free universe variable

Mario Carneiro (Sep 04 2020 at 10:37):

alternatively:

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

Fox Thomson (Sep 04 2020 at 10:39):

What is the to_expr function?

Mario Carneiro (Sep 04 2020 at 10:39):

tactic.to_expr

Mario Carneiro (Sep 04 2020 at 10:40):

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

Fox Thomson (Sep 04 2020 at 10:41):

Thank you


Last updated: Dec 20 2023 at 11:08 UTC