test-jcf.why 277 Bytes
Newer Older
1 2 3

(* test file *)

4
theory Test
5
  use import int.Int
6
  logic (*) int int
7
  goal G : forall x : int. 1 * 2 -> x * 3
8 9
end

10

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
11 12
(*
Local Variables: 
13
compile-command: "cd ..; bin/why.opt -D drivers/simplify.drv tests/test-jcf.why && bin/why.opt -P simplify tests/test-jcf.why"
Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
14 15
End: 
*)
16