Zulip Chat Archive

Stream: new members

Topic: dump expr to context

Kenny Lau (Nov 24 2018 at 16:02):

Is there a way to dump an expr to the context?

Rob Lewis (Nov 24 2018 at 16:22):

What do you mean?

Rob Lewis (Nov 24 2018 at 16:23):

tactic.pose?

Kenny Lau (Nov 24 2018 at 18:25):

@Rob Lewis that dumps the evaluated expression to the context; I want the unevaluated expression as an expr itself

Kevin Buzzard (Nov 24 2018 at 18:27):

You should learn to ask better questions Kenny.

Rob Lewis (Nov 24 2018 at 20:46):

You want a tactic that adds a local hypothesis of type expr, defined to be some particular expr that you have? Could you explain what you're trying to do? I kind of doubt this is the way to do it.

Chris Hughes (Nov 26 2018 at 10:41):

Can't you just use pose and give it `(e) , where e : expr?

Last updated: Dec 20 2023 at 11:08 UTC