e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskiclass Type < Type

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowskivar t : Type

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowskiclass TYPE < {x . x < t}

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskitype : Type- -> Type; Unit : TYPE

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiclass a, b, c < Type

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiclass a, b, c < Type; a < b

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskitype s : c

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskipred tt : s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskivar x : s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram (pred tt : s) = \ (var x : s) . ()

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram __ res __ (x : s, y : t) : s = x;

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski fst (x : s, y : t) : s = x; snd (x : s, y : t) : t = y

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskipred eq : s * s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskitype s < ? s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram all (p : (? s)) : (? Unit) = eq (p, tt)

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ()

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram __ impl __ (x, y : (? Unit)) = eq (x, x And y)

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiprogram __ or __ (x, y : (? Unit)) : (? Unit) =

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski ex (p : (? s)) : (? Unit) =

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski ff () : (? Unit) = all (\ r : (? Unit) . r ())

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiforall x : t; y : t

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski. %(..)%

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski (fun __=__[t] : forall a : Type . a * a ->? Unit)

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski (var x : t, var y : t)

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskitype s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiop a : ? s

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskitype Data1 ::= a |

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski b |

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski c

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskitype Data2 ::= Cons21 (Data1; Data2) |

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski Cons22 (Data2; Data1) |

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski type Data1

da955132262baab309a50fdffe228c9efe68251dCui Jiantype Data3 ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Cons32 (sel2 :? Data2; sel1 :? Data1)

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskitype Data4 ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Cons42 (sel2 :? Data2; sel1 :? Data1)?

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski. (fun true : Unit)

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowskiforall x : s

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowskiforall x : s

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski%% Classes ---------------------------------------------------------------

7474388b4c2236f8ab2327289555000268c7901aTill MossakowskiTYPE < {x . x < t}

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskia < b

da955132262baab309a50fdffe228c9efe68251dCui Jianb < Type

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskic < Type

8d6aa4bda97770cc79cf96de3c0f9dfa4d7d7aafChristian Maeder%% Type Constructors -----------------------------------------------------

99249aeda5fac6f8f0b2316ca357bac898af1928Christian MaederData1

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski : Type < Data2

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski %[type Data1

4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maeder ::= a : Data1

b : Data1

c : Data1]%

Data2

: Type

%[type Data2

::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)

Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)

types Data1]%

Data3

: Type

%[type Data3

::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)

Cons32 : Data2 * Data1 -> Data3 (sel2 :? Data2; sel1 :? Data1)]%

Data4

: Type

%[type Data4

::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)

Cons42 : Data2 * Data1 ->? Data4 (sel2 :? Data2; sel1 :? Data1)]%

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : TYPE := Unit

__*__ : Type+ -> Type+ -> Type

__-->__ : Type- -> Type+ -> Type

__-->?__ : Type- -> Type+ -> Type

__->__ : Type- -> Type+ -> Type

__->?__ : Type- -> Type+ -> Type

s : c < ? s

t : Type %(var)%

%% Assumptions -----------------------------------------------------------

Cons21 : Data1 * Data2 -> Data2 %(construct Data2)%

Cons22 : Data2 * Data1 -> Data2 %(construct Data2)%

Cons31 : Data1 * Data2 -> Data3 %(construct Data3)%

Cons32 : Data2 * Data1 -> Data3 %(construct Data3)%

Cons41 : Data1 * Data2 ->? Data4 %(construct Data4)%

Cons42 : Data2 * Data1 ->? Data4 %(construct Data4)%

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

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

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

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

__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

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

__if__ : Unit * Unit ->? Unit %(fun)%

__when__else__ : forall a : Type . a * Unit * a ->? a %(fun)%

a : Data1 %(construct Data1)%

: ? s %(op)%

b : Data1 %(construct Data1)%

c : Data1 %(construct Data1)%

def__ : forall a : Type . a ->? Unit %(fun)%

eq : s * s ->? Unit %(pred)%

false : Unit %(fun)%

if__then__else__ : forall a : Type . Unit * a * a ->? a %(fun)%

not__ : Unit ->? Unit %(fun)%

sel1

: Data4 ->? Data1

%(select from Data4 constructed by

(Cons41 : Data1 * Data2 ->? Data4,

Cons42 : Data2 * Data1 ->? Data4))%

: Data3 ->? Data1

%(select from Data3 constructed by

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

sel2

: Data4 ->? Data2

%(select from Data4 constructed by

(Cons41 : Data1 * Data2 ->? Data4,

Cons42 : Data2 * Data1 ->? Data4))%

: Data3 ->? Data2

%(select from Data3 constructed by

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

true : Unit %(fun)%

tt : s ->? Unit %(op)% = \ (var x : s) . ()

%% Sentences -------------------------------------------------------------

program (pred tt : s) = \ (var x : s) . () %(pe_tt)%

(fun __=__[t] : forall a : Type . a * a ->? Unit)

(var x : t, var y : t)

type Data1

::= a : Data1

b : Data1

c : Data1 %(ga_Data1)%

type Data2

::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)

Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)

types Data1 %(ga_Data2)%

forall x_1_1 : Data1; x_1_2 : Data2

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel1 : Data3 ->? Data1)

((op Cons31 : Data1 * Data2 -> Data3)

(var x_1_1 : Data1, var x_1_2 : Data2)),

var x_1_1 : Data1) %(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel2 : Data3 ->? Data2)

((op Cons31 : Data1 * Data2 -> Data3)

(var x_1_1 : Data1, var x_1_2 : Data2)),

var x_1_2 : Data2) %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel2 : Data3 ->? Data2)

((op Cons32 : Data2 * Data1 -> Data3)

(var x_1_1 : Data2, var x_1_2 : Data1)),

var x_1_1 : Data2) %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel1 : Data3 ->? Data1)

((op Cons32 : Data2 * Data1 -> Data3)

(var x_1_1 : Data2, var x_1_2 : Data1)),

var x_1_2 : Data1) %(ga_select_sel1)%

type Data3

::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)

Cons32 : Data2 * Data1 -> Data3

(sel2 :? Data2; sel1 :? Data1) %(ga_Data3)%

forall x_1_1 : Data1; x_1_2 : Data2

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel1 : Data4 ->? Data1)

((op Cons41 : Data1 * Data2 ->? Data4)

(var x_1_1 : Data1, var x_1_2 : Data2)),

var x_1_1 : Data1) %(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel2 : Data4 ->? Data2)

((op Cons41 : Data1 * Data2 ->? Data4)

(var x_1_1 : Data1, var x_1_2 : Data2)),

var x_1_2 : Data2) %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel2 : Data4 ->? Data2)

((op Cons42 : Data2 * Data1 ->? Data4)

(var x_1_1 : Data2, var x_1_2 : Data1)),

var x_1_1 : Data2) %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. (fun __=__ : forall a : Type . a * a ->? Unit)

((op sel1 : Data4 ->? Data1)

((op Cons42 : Data2 * Data1 ->? Data4)

(var x_1_1 : Data2, var x_1_2 : Data1)),

var x_1_2 : Data1) %(ga_select_sel1)%

type Data4

::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)

Cons42 : Data2 * Data1 ->? Data4

(sel2 :? Data2; sel1 :? Data1) %(ga_Data4)%

(fun true : Unit)

%% Diagnostics -----------------------------------------------------------

*** Error 1.7, illegal universe class declaration 'Type'

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

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

*** Error 11.16, undeclared class 'd'

*** Warning 11.7, redeclared class 'a'

*** Warning 11.10, redeclared class 'b'

*** Warning 11.13, redeclared class 'c'

*** Warning 11.19, redeclared class 'a'

*** Error 20.12, unexpected mixfix token: res

*** Hint 21.1, no type match for: fst

with type: '_var_3 ->? s' (21.20)

known types:

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

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

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

*** Hint 22.1, no type match for: snd

with type: '_var_4 ->? 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_5 ->? ? 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_7 ->? ? Unit' (30.32)

known types:

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

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

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

*** Error 32.12, unexpected mixfix token: impl

*** Error 34.12, unexpected mixfix token: or

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

with type: '_var_8 ->? ? 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_9 ->? ? 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