Janno (Jun 02 2020 at 17:24): Janno (Jun 02 2020 at 17:24):Is there a way to get generalized rewriting with stratagies to interact with ltac backtracking? Asked differently: is there any way to get the following to succeed?
From Coq Require Import Setoid.
Axiom lem1 : False -> 1+1=2.
Axiom lem2 : True -> 1+1=2.
Goal 1+1=2. (rewrite_strat subterms (choice lem1 lem2)); exact I. Qed.
I don't think rewrite_strat is a multi success tactic yes, but can certainly be turned into one (it's based on continuations already)
Janno (Jun 04 2020 at 12:38):I suppose now I understand what a multi-success tactic is. Thanks! :)
Could you give an estimate of what would be involved in making this change (or providing a separate version of rewrite_strat)?
Last updated: Sep 23 2023 at 08:01 UTC