test.why 834 Bytes
Newer Older
1 2 3

(* test file *)

4 5
theory A
  type t
6
  logic c : t
7 8 9
end

theory B
10 11 12 13 14
  namespace S type t end
  logic d : S.t
  logic f : S.t -> S.t
  logic p : S.t -> prop
  axiom Ax : forall x:S.t. p(x) or p(f(x))
15 16
end

17
theory Int
18 19 20
  type int
end

21
theory Eq 
22

23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
  logic eq : 'a, 'a -> prop 

  (* This part is just a definition of the equality *)

  (* This theory define eq but of course these axioms should not be send
   to provers *)
 
  axiom refl : forall x:'a. eq(x,x) 
  axiom sym  : forall x,y:'a. eq(x,y) -> eq(y,x)
  axiom trans : forall x,y,z:'a. eq(x,y) -> eq(y,z) -> eq(x,z)
  (* This one can't be written in first order logic. *)
  type t
  type u
  logic f : t -> u
  axiom congru : forall x,y:t. eq(x,y) -> eq(f(x),f(y))
38

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39
end
40

41
(*
42
theory Test
43

44 45
  use Eq
  use import L : List
46
  axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
47

48 49
end
*)