Lukas Stevens (Dec 06 2022 at 14:43): Lukas Stevens (Dec 06 2022 at 14:43):Is there a tactic that can instantiate schematic variables in the goal?
Manuel Eberl (Dec 08 2022 at 13:03):To my knowledge, no – at least not in the standard library. Probably not considered very good style either because schematic variables tend to have fairly unpredictable names. I guess you could instantiate them by position instead…
Manuel Eberl (Dec 08 2022 at 13:03):Peter Lammich might have something like this hidden away in the Autoref libraries somewhere…
Lukas Stevens (Dec 08 2022 at 16:11):Manuel Eberl said:
To my knowledge, no – at least not in the standard library. Probably not considered very good style either because schematic variables tend to have fairly unpredictable names. I guess you could instantiate them by position instead…
Yes, by position was the idea.
Last updated: Apr 20 2024 at 04:19 UTC