Restricting behavior of rewrite_list
Hello,
Currently rewrite_list
uses the argument with_terms
but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by apply/rewrite
after matching. For example,
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
rewrite <- A with 43 (* To instantiate a *)
rewrite <- B with 43 (* To instantiate a *)
To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
rewrite_list <- A,B with 43
Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?