Stream: Elpi users & devs

Topic: intropatterns in tactic

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

Hi,
I am making a tactic that needs as argument an intropattern. Is there a way to get a simple_intropattern(x) or simple_intropattern_list(x) as argument for an elpi tactic, and then use it in a call to intros?

view this post on Zulip Enrico Tassi (Sep 27 2023 at 14:06):

No, unfortunately not. I think I see your use case, please open an issue on coq-elpi and I'll see what I can do.

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

I have submitted an issue

view this post on Zulip Enrico Tassi (Sep 27 2023 at 14:15):

thanks

Last updated: Oct 13 2024 at 01:02 UTC