root/trunk/HasCASL/test/Graphs.hascasl.output @ 11877

Revision 11877, 5.0 kB (checked in by maeder, 5 months ago)

disallowed explicit pseudo type notation following := (assign)

  • Property svn:eol-style set to native
  • Property svn:keywords set to Author Date Id Revision
Line 
1vars  S, T : Type
2types Bool;
3      Pred S := S ->? Unit;
4      Set S := S ->? Unit
5ops   True, False : Bool
6ops   emptySet : Set S;
7      {__} : S -> Set S;
8      __isIn__ : S * Set S ->? Unit;
9      __subset__ : Pred (Set (S) * Set (S));
10      __union__, __intersection__, __\\__ : Set S * Set S -> Set S;
11      __disjoint__ : Pred (Set (S) * Set (S));
12      __*__ : Set S * Set T -> Set (S * T);
13      __disjointUnion__ : Set S * Set S -> Set (S * Bool);
14      inl, inr : S -> S * Bool
15forall x, x' : S; y : T; s, s' : Set S; t : Set T
16. not x isIn emptySet
17. x isIn { x' } <=> x = x'
18. x isIn s <=> s x
19. s subset s' <=> forall x : S . x isIn s => x isIn s'
20. x isIn (s union s') <=> x isIn s \/ x isIn s'
21. x isIn (s intersection s') <=> x isIn s /\ x isIn s'
22. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'
23. s disjoint s' <=> s intersection s' = emptySet
24. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t
25. inl x = (x, False)
26. inr x = (x, True);
27types
28Bool : Type;
29Set : Type -> Type
30type
31Set := \ S : Type . S ->? Unit
32vars
33S : Type %(var_1)%;
34T : Type %(var_2)%
35op False : Bool %(op)%
36op True : Bool %(op)%
37op __*__ : forall S : Type; T : Type . Set S * Set T -> Set (S * T)
38           %(op)%
39op __\\__ : forall S : Type . Set S * Set S -> Set S %(op)%
40op __disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%
41op __disjointUnion__ : forall S : Type
42                       . Set S * Set S -> Set (S * Bool)
43                       %(op)%
44op __intersection__ : forall S : Type . Set S * Set S -> Set S
45                      %(op)%
46op __isIn__ : forall S : Type . S * Set S ->? Unit %(op)%
47op __subset__ : forall S : Type . Pred (Set S * Set S) %(op)%
48op __union__ : forall S : Type . Set S * Set S -> Set S %(op)%
49op emptySet : forall S : Type . Set S %(op)%
50op inl : forall S : Type . S -> S * Bool %(op)%
51op inr : forall S : Type . S -> S * Bool %(op)%
52op {__} : forall S : Type . S -> Set S %(op)%
53forall S : Type; x : S . not x isIn emptySet
54forall S : Type; x : S; x' : S . x isIn { x' } <=> x = x'
55forall S : Type; s : Set S; x : S . x isIn s <=> s x
56forall S : Type; s : Set S; s' : Set S
57. s subset s' <=> forall x : S . x isIn s => x isIn s'
58forall S : Type; s : Set S; s' : Set S; x : S
59. x isIn (s union s') <=> x isIn s \/ x isIn s'
60forall S : Type; s : Set S; s' : Set S; x : S
61. x isIn (s intersection s') <=> x isIn s /\ x isIn s'
62forall S : Type; s : Set S; s' : Set S; x : S
63. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'
64forall S : Type; s : Set S; s' : Set S
65. s disjoint s' <=> s intersection s' = emptySet
66forall S : Type; T : Type; s : Set S; t : Set T; x : S; y : T
67. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t
68forall S : Type; x : S . inl x = (x, False)
69forall S : Type; x : S . inr x = (x, True)
70### Hint 1.6, is type variable 'S'
71### Hint 1.8, is type variable 'T'
72### Hint 3.14, rebound type variable 'S'
73### Hint 3.8, redeclared type 'Pred'
74### Hint 4.13, rebound type variable 'S'
75### Hint 9.18,
76no kind found for 'S'
77  expected: {Cpo}
78     found: {Type}
79### Hint 9.18,
80no kind found for 'S'
81  expected: {Cppo}
82     found: {Type}
83### Hint 10.25-10.29,
84no kind found for 'Set S'
85  expected: {Cpo}
86     found: {Type}
87### Hint 10.25-10.29,
88no kind found for 'Set S'
89  expected: {Cppo}
90     found: {Type}
91### Hint 11.46-11.50,
92no kind found for 'Set S'
93  expected: {Cpo}
94     found: {Type}
95### Hint 11.46-11.50,
96no kind found for 'Set S'
97  expected: {Cppo}
98     found: {Type}
99### Hint 11.46-11.50,
100no kind found for 'Set S'
101  expected: {Cpo}
102     found: {Type}
103### Hint 11.46-11.50,
104no kind found for 'Set S'
105  expected: {Cppo}
106     found: {Type}
107### Hint 11.46-11.50,
108no kind found for 'Set S'
109  expected: {Cpo}
110     found: {Type}
111### Hint 11.46-11.50,
112no kind found for 'Set S'
113  expected: {Cppo}
114     found: {Type}
115### Hint 12.28-12.32,
116no kind found for 'Set S'
117  expected: {Cpo}
118     found: {Type}
119### Hint 12.28-12.32,
120no kind found for 'Set S'
121  expected: {Cppo}
122     found: {Type}
123### Hint 13.15-13.19,
124no kind found for 'Set S'
125  expected: {Cpo}
126     found: {Type}
127### Hint 13.15-13.19,
128no kind found for 'Set S'
129  expected: {Cppo}
130     found: {Type}
131### Hint 13.37,
132no kind found for 'S'
133  expected: {Cpo}
134     found: {Type}
135### Hint 13.37,
136no kind found for 'S'
137  expected: {Cppo}
138     found: {Type}
139### Hint 14.28-14.32,
140no kind found for 'Set S'
141  expected: {Cpo}
142     found: {Type}
143### Hint 14.28-14.32,
144no kind found for 'Set S'
145  expected: {Cppo}
146     found: {Type}
147### Hint 14.50,
148no kind found for 'S'
149  expected: {Cpo}
150     found: {Type}
151### Hint 14.50,
152no kind found for 'S'
153  expected: {Cppo}
154     found: {Type}
155### Hint 15.22,
156no kind found for 'S'
157  expected: {Cpo}
158     found: {Type}
159### Hint 15.22,
160no kind found for 'S'
161  expected: {Cppo}
162     found: {Type}
163### Hint 15.22,
164no kind found for 'S'
165  expected: {Cpo}
166     found: {Type}
167### Hint 15.22,
168no kind found for 'S'
169  expected: {Cppo}
170     found: {Type}
171### Hint 16.11, not a class 'S'
172### Hint 16.14, not a class 'S'
173### Hint 16.19, not a class 'T'
174### Hint 16.24, not a kind 'Set (S)'
175### Hint 16.27, not a kind 'Set (S)'
176### Hint 16.37, not a kind 'Set (T)'
177### Hint 20.32, not a class 'S'
178### Hint 20.31, rebound variable 'x'
Note: See TracBrowser for help on using the browser.