test.why 306 Bytes
Newer Older
1 2 3

(* test file *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
theory Test1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
5 6 7
  use import prelude.Int
  axiom Ax : forall x :int. x=1 and forall x:int. x=2
  logic g(x: int) : int = x+2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14
end

theory Test
  use graph.Path
  use import prelude.List
  axiom Ax : forall l:int list. l=l
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
16 17 18 19 20
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)