GitLab

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 ?