2b873214c9ab511bbca437c036371ab664aedaceChristian Maederclass Type < Type

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedervar t : Type

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maederclass TYPE < {x . x < t}

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maedertype : Type- -> Type; Unit : TYPE

54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian Maederclass a, b, c < Type

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiclass a, b, c < Type; a < b

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maedertype s : c

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskipredfun tt : s ->? Unit

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskivar x : s

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederprogram (predfun tt : s ->? Unit) = \ (var x : s) . ()

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederprogram __ res __ (x : s, y : t) : s : s = x;

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder fst (x : s, y : t) : s = x; snd (x : s, y : t) : t = y

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederpredfun eq : s � s ->? Unit

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedertype s < ? s

da955132262baab309a50fdffe228c9efe68251dCui Jianprogram all (p : (? s)) : (? Unit) = eq (p, tt)

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederprogram And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ()

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederprogram __ impl __ (x, y : (? Unit)) = eq (x, x And y)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederprogram __ or __ (x, y : (? Unit)) : ? Unit : ? Unit =

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder ex (p : (? s)) : (? Unit) =

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder ff () : (? Unit) = all (\ r : (? Unit) . r ())

52d922076b89f12234f721974e82531bc69a6f69Christian Maederforall x : t; y : t

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder. %(..)%

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

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder (var y : t))

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maedertype s

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederop a : ? s

14c89b2d830777bf4db2850f038c9f60acaca486Christian Maedertype Data1 ::= a |

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski b |

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder c

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maedertype Data2 ::= Cons21 (Data1; Data2) |

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder Cons22 (Data2; Data1) |

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder type Data1

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedertype Data3 ::= Cons31 (sel1:? Data1; sel2:? Data2) |

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Cons32 (sel2:? Data2; sel1:? Data1)

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröningtype Data4 ::= Cons41 (sel1:? Data1; sel2:? Data2) ? |

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Cons42 (sel2:? Data2; sel1:? Data1) ?

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu. (fun true : Unit)

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grossforall x : s

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederforall x : s

a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder%% Classes ---------------------------------------------------------------

0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von SchroederTYPE < {x . x < t}

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maedera < b

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanub < Type

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Grossc < Type

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder%% Type Constructors -----------------------------------------------------

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederData1 : Type < Data2 %[type __ ::=

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder a : -> __

6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder b : -> __

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl c : -> __]%

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovaData2 : Type %[type __ ::=

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz Cons21 : Data1 � Data2 -> __

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Cons22 : Data2 � Data1 -> __]%

14c89b2d830777bf4db2850f038c9f60acaca486Christian MaederData3 : Type %[type __ ::=

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Cons31 : Data1 � Data2 -> __ (sel1 :? Data1)(sel2 :? Data2)

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Cons32 : Data2 � Data1 -> __ (sel2 :? Data2)(sel1 :? Data1)]%

57026bc09337d158b89775048a9bcc9c17d825caChristian MaederData4 : Type %[type __ ::=

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder Cons41 : Data1 � Data2 ->? __ (sel1 :? Data1)(sel2 :? Data2)

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Cons42 : Data2 � Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1)]%

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin KühlPred : Type -> Type := \ a : Type . a ->? Unit

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederUnit : TYPE := Unit

2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder__-->__ : Type- -> Type+ -> Type

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder__-->?__ : Type- -> Type+ -> Type

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder__->__ : Type- -> Type+ -> Type

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder__->?__ : Type- -> Type+ -> Type

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

52d922076b89f12234f721974e82531bc69a6f69Christian Maeders : c < ? s

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grosst : Type %(var)%

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross%% Assumptions -----------------------------------------------------------

9175e29c044318498a40f323f189f9dfd50378efChristian MaederCons21 : Data1 � Data2 -> Data2 %(construct Data2)%

9175e29c044318498a40f323f189f9dfd50378efChristian MaederCons22 : Data2 � Data1 -> Data2 %(construct Data2)%

52d922076b89f12234f721974e82531bc69a6f69Christian MaederCons31 : Data1 � Data2 -> Data3 %(construct Data3)%

9175e29c044318498a40f323f189f9dfd50378efChristian MaederCons32 : Data2 � Data1 -> Data3 %(construct Data3)%

9175e29c044318498a40f323f189f9dfd50378efChristian MaederCons41 : Data1 � Data2 ->? Data4 %(construct Data4)%

9175e29c044318498a40f323f189f9dfd50378efChristian MaederCons42 : Data2 � Data1 ->? Data4 %(construct Data4)%

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

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder__<=>__ : Unit � Unit ->? Unit %(Fun)%

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

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder__=>__ : Unit � Unit ->? Unit %(Fun)%

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

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

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder__if__ : Unit � Unit ->? Unit %(Fun)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maedera : Data1 %(construct Data1)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder : ? s %(Op)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maederb : Data1 %(construct Data1)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maederc : Data1 %(construct Data1)%

9175e29c044318498a40f323f189f9dfd50378efChristian Maederdef__ : forall a : Type . a ->? Unit %(Fun)%

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühleq : s � s ->? Unit %(Pred)%

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlfalse : Unit %(Fun)%

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

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedernot__ : Unit ->? Unit %(Fun)%

52d922076b89f12234f721974e82531bc69a6f69Christian Maedersel1 : Data4 ->? Data1 %(select from Data4 constructed by

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Cons41 : Data1 � Data2 ->? Data4,

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Cons42 : Data2 � Data1 ->? Data4))%

bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas : Data3 ->? Data1 %(select from Data3 constructed by

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder (Cons31 : Data1 � Data2 -> Data3,

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Cons32 : Data2 � Data1 -> Data3))%

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maedersel2 : Data4 ->? Data2 %(select from Data4 constructed by

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder (Cons41 : Data1 � Data2 ->? Data4,

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Cons42 : Data2 � Data1 ->? Data4))%

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder : Data3 ->? Data2 %(select from Data3 constructed by

7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder (Cons31 : Data1 � Data2 -> Data3,

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder Cons32 : Data2 � Data1 -> Data3))%

63719301448519453f66383f4e583d9fd5b89ecbChristian Maedertrue : Unit %(Fun)%

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedertt : s ->? Unit %(Op)% = \ (var x : s) . ()

0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder%% Sentences -------------------------------------------------------------

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

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder (var y : t)) %()%

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl(fun true : Unit) %()%

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova%% Diagnostics -----------------------------------------------------------

72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz*** Error 1.7, illegal universe class declaration 'Type'

a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder*** Hint 3.5, is type variable 't'

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder*** FatalError 7.11, illegal type pattern argument: __

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder*** Error 11.16, undeclared class 'd'

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder*** Warning 11.7, redeclared class 'a'

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder*** Warning 11.10, redeclared class 'b'

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder*** Warning 11.13, redeclared class 'c'

bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von Schroeder*** Warning 11.19, redeclared class 'a'

b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder*** Error 20.12, unexpected mixfix token: res

b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder*** Error 20.10, unexpected term '__ res __ (x : s, y : t)'

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross*** Error 20.37, unexpected mixfix token: x

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross*** Hint 21.1, no type match for: fst

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer with type: '_var_4 ->? s' (21.20)

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer known types:

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder*** Hint 21.1, wrong result type 's' (21.20)

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder for application 'fst ((var x : s), (var y : t))'

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich*** Error 21.1, no typing for 'fst(((var x : s), (var y : t))) : s'

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder*** Hint 22.1, no type match for: snd

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder with type: '_var_5 ->? t' (22.20)

known types:

*** Hint 22.1, wrong result type 't' (22.20)

for application 'snd ((var x : s), (var y : t))'

*** Error 22.1, no typing for 'snd(((var x : s), (var y : t))) : t'

*** Hint 28.9, no type match for: all

with type: '_var_6 ->? ? Unit' (28.27)

known types:

*** Hint 28.9, wrong result type '? Unit' (28.27)

for application 'all (var p : ? s)'

*** Error 28.9, no typing for 'all((var p : ? s)) : ? Unit'

*** Hint 30.9, no type match for: And

with type: '_var_8 ->? ? Unit' (30.32)

known types:

*** Hint 30.9, wrong result type '? Unit' (30.32)

for application 'And ((var x : _var_7), (var y : ? Unit))'

*** Error 30.9, no typing for 'And(((var x : _var_7), (var y : ? Unit))) : ? Unit'

*** Error 32.12, unexpected mixfix token: impl

*** Error 34.12, unexpected mixfix token: or

*** Error 34.10, unexpected term '__ or __ (x, y : (? Unit))'

*** Error 35.19, unexpected mixfix token: x

*** Error 34.44, unexpected mixfix token: all

*** Hint 37.3, no type match for: ex

with type: '_var_10 ->? ? Unit' (37.19)

known types:

*** Hint 37.3, wrong result type '? Unit' (37.19)

for application 'ex (var p : ? s)'

*** Error 37.3, no typing for 'ex((var p : ? s)) : ? Unit'

*** Hint 40.3, no type match for: ff

with type: '_var_11 ->? ? Unit' (40.12)

known types:

*** Hint 40.3, wrong result type '? Unit' (40.12)

for application 'ff ()'

*** Error 40.3, no typing for 'ff(()) : ? Unit'

*** Error 66.25, unexpected mixfix token: e

*** Error 67.12, unexpected mixfix token: e