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):
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
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