Zulip Chat Archive

Stream: new members

Topic: dump expr to context


view this post on Zulip Kenny Lau (Nov 24 2018 at 16:02):

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

view this post on Zulip Rob Lewis (Nov 24 2018 at 16:22):

What do you mean?

view this post on Zulip Rob Lewis (Nov 24 2018 at 16:23):

tactic.pose?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 18:27):

You should learn to ask better questions Kenny.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 26 2018 at 10:41):

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


Last updated: May 18 2021 at 16:25 UTC