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)
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
Last updated: Sep 23 2023 at 08:01 UTC