Stream: Elpi users & devs

Topic: ✔ renaming when opening a sealed goal

view this post on Zulip Enrico Tassi (Sep 25 2023 at 12:02):

I think you should run open first.
I mean, you can, but you would also have to match on the context, eg msolve [nabla P\seal (goal _ {{ lp:P -> lp:P }} _ _ )].. not easy. (that would be you previous goal).

view this post on Zulip Luko van der Maas (Sep 25 2023 at 12:17):

Thanks, than I will do that

view this post on Zulip Notification Bot (Sep 25 2023 at 12:44):

Luko van der Maas has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC