test.why 387 Bytes
Newer Older
1 2 3

(* test file *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
theory A
5
  use import prelude.Int
6 7
  logic p(int, int)
  axiom A : forall x,y:int, z,t:real. x=x
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10
end

theory TreeForest
11 12 13
  type 'a list = Nil | Cons('a, 'a list)
  type 'a tree = Leaf('a) | Node('a forest)
  type 'a forest = 'a tree list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
14 15
end

16
theory TestPrelude 
17
  use prelude.Int
18 19
  use prelude.List
end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
20

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

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