HasCASL/test/SuperClassWarnings.hascasl.output

	SuperClassWarnings.hascasl.output revision 02535bb32f01cbb935f41f8ccb957ebb5c1091c6


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
%% all warnings
class a < b
      %% implicit super class declaration
class b
      %% redeclared class
class c < Type
      %% useless (always true)
class d < a
      %% ok
class d < b
      %% transitive via a
class d < a
      %% direct repetition
class e < f
      %% Type is silently ignored
class g < h
      %% doubles are silently ignored
%% Classes ---------------------------------------------------------------
a < b
b
c
d < (a, b)
e < f
f
g < h
h
%% Type Constructors -----------------------------------------------------
Pred : Type -> Type := \ a : Type . a ->? Unit
Unit : Type := Unit
%% Assumptions -----------------------------------------------------------
__/\__ : Unit � Unit ->? Unit
__<=>__ : Unit � Unit ->? Unit
__=__ : forall a : Type .  a � a ->? Unit
__=>__ : Unit � Unit ->? Unit
__=e=__ : forall a : Type .  a � a ->? Unit
__\/__ : Unit � Unit ->? Unit
def__ : forall a : Type .  a ->? Unit
if__then__else__ : forall a : Type .  Unit � a � a ->? a
not__ : Unit ->? Unit
%% Diagnostics -----------------------------------------------------------
Warning (line 2, column 11) implicit declaration of superclass 'b'
Warning (line 3, column 7) redeclared class 'b'
Warning (line 4, column 11) redundant universe class
Warning (line 6, column 7) redeclared class 'd'
Warning (line 6, column 11) already known as super class 'b'
Warning (line 7, column 7) redeclared class 'd'
Warning (line 7, column 11) already known as super class 'a'
Warning (line 8, column 18) implicit declaration of superclass 'f'
Warning (line 9, column 12) implicit declaration of superclass 'h'