8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettclass a, b, c, d < Type

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maedertype r, s, t

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowskitype [__], {__} : a -> b

63f8854d42e766ff77125c6e532c5fce3b5ebdefChristian Maedervar u : [r]; v : {s}

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescutype tuple3 : a -> b -> c -> d

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettvar x : tuple3 r s t

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimbletttype tuple1 : b -> a

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimbletttype m : (a -> b) -> c

63f8854d42e766ff77125c6e532c5fce3b5ebdefChristian Maedertype List : a -> b

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettvar v : m List

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettvar nt : a -> (b -> c) -> c -> d

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimbletttype s1, r1, t1 < t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimbletttype s2 = r2 = t2

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maedertype s3 = {x : t . ((fun __=__[t]

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder t * t ->? Unit)

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder (var x : t, var x : t) :

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder Unit}

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett%% Classes ---------------------------------------------------------------

9f93b2a8b552789cd939d599504d39732672dc84Christian Maedera < Type

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettb < Type

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettc < Type

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettd < Type

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett%% Type Constructors -----------------------------------------------------

c3f3b3166ed4c19c72a27a2d6f8176730e94e71eAndy GimblettList : a -> b

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettLogical : Type := Unit ->? Unit

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederUnit : Type

5d48a25007fbfa021ca32df2d75770c02d531285Andy Gimblett[__] : a -> b

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__*__ : +Type -> +Type -> Type

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__->__ : -Type -> +Type -> Type < __->?__

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__->?__ : -Type -> +Type -> Type

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

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maedernt : a -> (b -> c) -> c -> d %(var_1)%

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettr : Type

53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblettr1 : Type < t

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederr2 : Type < (t2, r2, s2)

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeders : Type

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeders1 : Type < t

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeders2 : Type < (t2, r2, s2)

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeders3

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett : Type < t

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder = {x : t . ((fun __=__[t]

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder t * t ->? Unit)

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (var x : t, var x : t) :

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett Unit}

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyt : Type

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyt1 : Type < t

ef1de2a94f526fb52cba8fa9500e2b27d71fb8a6Andy Gimblettt2 : Type < (t2, r2, s2)

b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy Gimbletttuple1 : b -> a

9f93b2a8b552789cd939d599504d39732672dc84Christian Maedertuple3 : a -> b -> c -> d

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder{__} : a -> b

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett%% Assumptions -----------------------------------------------------------

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett__when__else__

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederbottom : forall a : Type . a_v-1 %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederfalse : Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maedernot__ : ? Unit ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maedertrue : Unit %(fun)%

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettu : [r] %(var)%

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettv : m List %(var)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder : {s} %(var)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederx : tuple3 r s t %(var)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder�__ : ? Unit ->? Unit %(fun)%

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder%% Diagnostics -----------------------------------------------------------

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder*** Hint 7.6, not a kind '[r]'

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder*** Hint 7.14, not a kind '{s}'

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder*** Hint 11.7, not a kind 'tuple3 r s t'

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder*** Hint 12.7, not a kind 'tuple3 r s'

*** Error, incompatible kind of: tuple3 r s

expected: Type

found: c -> d

*** Hint 18.7, not a kind 'm [__]'

*** Error 18.12, unexpected place '__'

*** Hint 22.7, not a kind 'm List'

*** Hint 24.8, not a class 'm'

*** Error 24.10, incompatible kind of: m

expected: Type

found: (a -> b) -> c

*** Hint 26.8, not a kind 'm tuple1'

*** Error 26.12, incompatible kind of: tuple1

expected: a -> b

found: b -> a

*** Hint 28.8, not a kind 'm tuple3'

*** Error 28.12, incompatible kind of: tuple3

expected: a -> b

found: a -> b -> c -> d

*** Hint 30.5, is type variable 'nt'

*** Hint 32.8, not a kind 'nt r List s'

*** Error 32.15, incompatible kind of: List

expected: b -> c

found: a -> b

*** Hint 38.12, variable shadows global name(s) 'x'