test.why 474 Bytes
Newer Older
1 2 3

(* test file *)

4 5 6 7 8 9
theory ThA
  type test
  logic test (test : test) : test
  goal Test : forall test : test . forall test : test . test(test) <> test
end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10
theory Test
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12
  use import prelude.Int
  logic id(x: int) : int = x
13 14
  logic id2(x: int) : int = id(x)
  logic succ(x:int) : int = id(x+1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15
  logic even(x: int) = 2*(x/2) = x
16
  goal G : forall x:int. 1 = succ(id2(zero))
Francois Bobot's avatar
Francois Bobot committed
17
  goal G2 : forall x:int. 0 = 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
20 21 22 23 24
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)
25