## 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: May 18 2021 at 16:25 UTC