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: Apr 20 2024 at 05:01 UTC