test.why 681 Bytes
Newer Older
1
2
3

(* test file *)

4
5
6
7
8
9
10
theory int

  type int

end

theory list
11

Jean-Christophe Filliâtre's avatar
uses    
Jean-Christophe Filliâtre committed
12
13
  uses int

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
14
  type 'a list
15

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
16
  logic nil  : 'a list
17

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

20
  logic is_nil : 'a list -> prop
21

22
  logic length : 'a list -> int.int
23

24
end
25

26
theory eq 
27

28
  logic eq : 'a, 'a -> prop
29

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
end
31

32
theory set
33

Jean-Christophe Filliâtre's avatar
uses    
Jean-Christophe Filliâtre committed
34
35
  uses eq

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36
  type elt
37

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
  type t 
39

40
41
42
43
44
45
  logic In : elt, t -> prop

  logic empty : t

  axiom empty_def1 : forall x:elt, not In(x, empty)

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

48
49
50
  axiom add_def1 : forall x,y:elt, forall s:t, 
                   In(x, add(y, s)) <-> (eq.eq(x, y) or In(x, s))

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
51
end
52
53
54

theory test

Jean-Christophe Filliâtre's avatar
uses    
Jean-Christophe Filliâtre committed
55
56
57
  uses eq, list

  axiom a : forall x : 'a, not eq.eq(list.nil, list.cons(list.nil, list.nil))
58
59
60

end