test_rewrite.mlw 194 Bytes
Newer Older
1 2 3 4 5 6


module M

  predicate (-->) (x y:'a) = "rewrite" x = y

7
  use int.Int
8 9 10 11 12 13 14 15

  goal g0 :
     forall x:int. ("rewrite" x = 42) -> x+1 = 42+1

  goal g :
     forall x:int. x --> 42 -> x+1 = 42

end