test.why 685 Bytes
Newer Older
1 2 3

(* test file *)

4
theory Int
5 6 7 8 9

  type int

end

10
theory List
11

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

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

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

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
  logic in_ : elt, t -> prop
41 42 43

  logic empty : t

44
  axiom empty_def1 : forall x:elt, not in_(x, empty)
45

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

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

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

theory test

55
  uses Eq, List
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
56

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

end