ca010363454de207082dfaa4b753531ce2a34551Christian Maeder%% all warnings

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass a < b

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder %% implicit super class declaration

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederclass b

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder %% redeclared class

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass c < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder %% useless (always true)

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass d < a

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder %% ok

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass d < b

46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder %% transitive via a

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass d < a

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder %% direct repetition

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass e < f

8b39fe4e459a2c534b55bab3bd68f929ba9a8b74Christian Maeder %% Type is silently ignored

ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass g < h

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder %% doubles are silently ignored

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder%% Classes ---------------------------------------------------------------

ca010363454de207082dfaa4b753531ce2a34551Christian Maedera < b

88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maederb

ca010363454de207082dfaa4b753531ce2a34551Christian Maederc

fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maederd < (a, b)

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maedere < f

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederf

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederg < h

9379646a4fecb772e793a8875bb92723e854268cChristian Maederh

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder%% Type Constructors -----------------------------------------------------

8b39fe4e459a2c534b55bab3bd68f929ba9a8b74Christian MaederPred : Type -> Type := \ a : Type . a ->? Unit

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian MaederUnit : Type := Unit

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder%% Assumptions -----------------------------------------------------------

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder__/\__ : Unit � Unit ->? Unit

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder__<=>__ : Unit � Unit ->? Unit

cf58a323fcb5c4185c3aa378713bbee3bba18c0aChristian Maeder__=__ : forall a : Type . a � a ->? Unit

cf58a323fcb5c4185c3aa378713bbee3bba18c0aChristian Maeder__=>__ : Unit � Unit ->? Unit

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder__=e=__ : forall a : Type . a � a ->? Unit

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder__\/__ : Unit � Unit ->? Unit

aae44eae4cd27141bea70af8d54844c3849a0711Christian Maederdef__ : forall a : Type . a ->? Unit

aae44eae4cd27141bea70af8d54844c3849a0711Christian Maederif__then__else__ : forall a : Type . Unit � a � a ->? a

ca010363454de207082dfaa4b753531ce2a34551Christian Maedernot__ : Unit ->? Unit

1db126da06f707b90b5be9d66a73c36ee2cd22eeChristian Maeder%% Diagnostics -----------------------------------------------------------

8b39fe4e459a2c534b55bab3bd68f929ba9a8b74Christian MaederWarning (line 2, column 11) implicit declaration of superclass 'b'

48708376ccab0e56251f53b0ec21499a277e9102Christian MaederWarning (line 3, column 7) redeclared class 'b'

1db126da06f707b90b5be9d66a73c36ee2cd22eeChristian MaederWarning (line 4, column 11) redundant universe class

1db126da06f707b90b5be9d66a73c36ee2cd22eeChristian MaederWarning (line 6, column 7) redeclared class 'd'

ca010363454de207082dfaa4b753531ce2a34551Christian MaederWarning (line 6, column 11) already known as super class 'b'

08f8731b34de5dc1ced274594978ad8879c831bdChristian MaederWarning (line 7, column 7) redeclared class 'd'

08f8731b34de5dc1ced274594978ad8879c831bdChristian MaederWarning (line 7, column 11) already known as super class 'a'

08f8731b34de5dc1ced274594978ad8879c831bdChristian MaederWarning (line 8, column 18) implicit declaration of superclass 'f'

d601fb0d7be0f4e8de9f01b5293df7d80673d76aChristian MaederWarning (line 9, column 12) implicit declaration of superclass 'h'

8b39fe4e459a2c534b55bab3bd68f929ba9a8b74Christian Maeder