Michael Soegtrop (Feb 22 2023 at 13:11): Michael Soegtrop (Feb 22 2023 at 13:11):I am currently looking for solutions for the issue I outlined here. How difficult would it be to have a with_strategy command in Ltac2, which takes a reference list? It would also be nice to have an abstract tactic, but since it doesn't take arguments one can easily redirect it to Ltac1.
Gaëtan Gilbert (Feb 22 2023 at 13:11):probably pretty easy
Gaëtan Gilbert (Feb 22 2023 at 13:25):are you going to make a PR?
Michael Soegtrop (Feb 22 2023 at 13:26):I guess one issue might be to create the parser for the specific syntax of with_strategy, but I am interested in a function without notation only.
Michael Soegtrop (Feb 22 2023 at 13:28):Gaëtan Gilbert said:
are you going to make a PR?
I would prefer to prioritise Coq Platform issues - e.g. the snap CI is currently broken and it is not trivial to fix (Ubuntu messed up LXD).
Last updated: Apr 19 2024 at 08:01 UTC