ca010363454de207082dfaa4b753531ce2a34551Christian Maederclass a, b, c, d < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maedertype r, s, t

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertype [__], {__} : a -> b

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedervar u : [r]; v : {s}

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maedertype tuple3 : a -> b -> c -> d

ca010363454de207082dfaa4b753531ce2a34551Christian Maedervar x : tuple3 r s t

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maedervar y : tuple3 r s

ca010363454de207082dfaa4b753531ce2a34551Christian Maedertype tuple1 : b -> a

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedertype m : (a -> b) -> c

ca010363454de207082dfaa4b753531ce2a34551Christian Maedervar

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maedertype List : a -> b

ca010363454de207082dfaa4b753531ce2a34551Christian Maedervar v : m List

ca010363454de207082dfaa4b753531ce2a34551Christian Maedervar o1 : m

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedervar o2 : m tuple1

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedervar o3 : m tuple3

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maedervar nt : a -> (b -> c) -> c -> d

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedervar o4 : nt r List s

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedertype s1, r1, t1 < t

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedertype s2 = r2 = t2

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedertype s3 : Type := t

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder%% Classes ---------------------------------------------------------------

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedera < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maederb < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maederc < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maederd < Type

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder%% Type Constructors -----------------------------------------------------

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederList : a -> b

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederPred : Type -> Type := \ a : Type . a ->? Unit

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederUnit : Type := Unit

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder[__] : a -> b

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder__-->__ : Type- -> Type+ -> Type

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder__-->?__ : Type- -> Type+ -> Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder__->__ : Type- -> Type+ -> Type

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder__->?__ : Type- -> Type+ -> Type

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder__�__ : Type+ -> Type+ -> Type

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederm : (a -> b) -> c

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maedernt : a -> (b -> c) -> c -> d %(var)%

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederr : Type

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederr1 : Type < t

028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maederr2 : Type < s2

975642b989852fc24119c59cf40bc1af653608ffChristian Maeders : Type

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeders1 : Type < t

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeders2 : Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeders3 : Type := t

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedert : Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedert1 : Type < t

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedert2 : Type < s2

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertuple1 : b -> a

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maedertuple3 : a -> b -> c -> d

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder{__} : a -> b

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder%% Assumptions -----------------------------------------------------------

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder__/\__ : Unit � Unit ->? Unit %(Fun)%

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder__<=>__ : Unit � Unit ->? Unit %(Fun)%

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder__=__ : forall a : Type . a � a ->? Unit %(Fun)%

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder__=>__ : Unit � Unit ->? Unit %(Fun)%

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder__\/__ : Unit � Unit ->? Unit %(Fun)%

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder__if__ : Unit � Unit ->? Unit %(Fun)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederdef__ : forall a : Type . a ->? Unit %(Fun)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederfalse : Unit %(Fun)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederif__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedernot__ : Unit ->? Unit %(Fun)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedero1 : m %(var)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedero2 : m tuple1 %(var)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedero3 : m tuple3 %(var)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedero4 : nt r List s %(var)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maedertrue : Unit %(Fun)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederu : [r] %(var)%

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederv : m List %(var)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder : {s} %(var)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederx : tuple3 r s t %(var)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maedery : tuple3 r s %(var)%

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder%% Diagnostics -----------------------------------------------------------

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder*** Error 12.9, incompatible kind of: tuple3 r s

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder expected: Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder found: c -> d

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder*** Error 18.12, unexpected place '__'

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder*** Error 24.10, incompatible kind of: m

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder expected: Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder found: (a -> b) -> c

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 26.12, incompatible kind of: tuple1

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder expected: a -> b

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder found: b -> a

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 28.12, incompatible kind of: tuple3

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder expected: a -> b

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder found: a -> b -> c -> d

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Hint 30.5, is type variable 'nt'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 32.15, incompatible kind of: List

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder expected: b -> c

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder found: a -> b

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.6, cyclic super type 's2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.9, cyclic super type 'r2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.9, cyclic super type 'r2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.9, cyclic super type 'r2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.12, cyclic super type 't2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.12, cyclic super type 't2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 36.12, cyclic super type 't2'

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder*** Error 38.19, ambiguous typings

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder '(fun __=__ : forall a : Type . a � a ->? Unit) ((var x : t),

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder (var x : t))' (38.19)

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder '(fun __=__ : forall a : Type . a �

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder a ->? Unit) ((var x : tuple3 r s t), (var x : tuple3 r s t))' (38.19)

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder