test.why 237 Bytes
Newer Older
1 2 3

(* test file *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
theory Test
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
5
  use import prelude.Int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6
  use BuiltIn
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7 8
  logic id(x: int) : int = x
  logic even(x: int) = 2*(x/2) = x
9
  goal G : forall x:int. 0 = zero
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
12 13 14 15 16
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)