test.why 866 Bytes
Newer Older
1 2 3

(* test file *)

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

theory B
  uses A
11 12 13
  open A
  logic d : t
  logic p : t -> prop
14 15 16
end

theory C
17
  uses B
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18
  uses T : B.A 
19
  logic e : T.t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
20
  axiom test : B.p(T.c)
21 22
end

23
theory Int
24 25 26
  type int
end

27
theory List
28

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29
  type 'a list
30

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
  logic nil  : 'a list
32

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33
  logic cons : 'a, 'a list -> 'a list
34

35
  logic is_nil : 'a list -> prop
36

37 38 39 40
  uses Int 
  open Int
  
  logic length : 'a list -> int
41

42
end
43

44
theory Eq 
45

46
  logic eq : 'a, 'a -> prop
47

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48
end
49

50
theory Set
51

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52
  type elt
53

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
54
  type t 
55

56
  logic in_ : elt, t -> prop
57 58 59

  logic empty : t

60
  axiom empty_def1 : forall x:elt. not in_(x, empty)
61

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62
  logic add : elt, t -> t
63

64 65 66
  uses Eq

  axiom add_def1 : forall x,y:elt. forall s:t.
67
                   in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
68

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69
end
70

71
theory Test
72

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
73
  uses Eq, L : List
74 75
  open L
  axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
76 77 78

end