Stream: Coq users

Topic: Ltac matching on multiple goals

view this post on Zulip Andres Erbsen (Oct 14 2020 at 15:51):

Is there a way to write anLltac that extracts a subterm from one goal to use it in another?

Last updated: Oct 05 2023 at 02:01 UTC