tests/test_rewrite.mlw

   1
   2
   3 module M
   4
   5   predicate (-->) (x y:'a) = "rewrite" x = y
   6
   7   use int.Int
   8
   9   goal g0 :
  10      forall x:int. ("rewrite" x = 42) -> x+1 = 42+1
  11
  12   goal g :
  13      forall x:int. x --> 42 -> x+1 = 42
  14
  15 end