class Type < Type

var t : Type

class TYPE < Type

type Unit : TYPE

class a, b, c < Type

class a, b, c < Type; a < b

type s : c

pred tt : s

var x : s

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

pred eq : s * s

type s < ? s

forall x : t; y : t

. %(..)%

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

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

type s

op a : (? s)

type Data1 ::= a |

b |

c

type Data2 ::= Cons21 (Data1; Data2) |

Cons22 (Data2; Data1) |

type Data1

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

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

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

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

. (fun true : Unit)

forall x : s

forall x : s

%% Classes ---------------------------------------------------------------

TYPE < Type

a < b

b < Type

c < Type

%% Type Constructors -----------------------------------------------------

? : +Type -> Type

Data1

: Type < Data2

%[type Data1

::= 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)]%

Logical : Type := ? Unit

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

Unit : (TYPE, Type)

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

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

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

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

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

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

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

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

s : (Type, c)

%% Type Variables --------------------------------------------------------

t : Type %(var_1)%

%% 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)%

bottom : forall a : Type . a %(fun)%

c : Data1 %(construct Data1)%

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

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

false : Unit %(fun)%

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

sel1

: Data4 ->? Data1

%(select from Data4 constructed by

(Cons42 : Data2 * Data1 ->? Data4,

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

: Data3 ->? Data1

%(select from Data3 constructed by

(Cons32 : Data2 * Data1 -> Data3,

Cons31 : Data1 * Data2 -> Data3))%

sel2

: Data4 ->? Data2

%(select from Data4 constructed by

(Cons42 : Data2 * Data1 ->? Data4,

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

: Data3 ->? Data2

%(select from Data3 constructed by

(Cons32 : Data2 * Data1 -> Data3,

Cons31 : Data1 * Data2 -> Data3))%

true : Unit %(fun)%

tt : s ->? Unit %(pred)%

�__ : ? Unit ->? Unit %(fun)%

%% Variables -------------------------------------------------------------

x : s

y : t

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

program tt = \ x . () %(pe_tt)%

x = y

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

. ((op sel1 : Data3 ->? Data1) (Cons31 (x_1_1, x_1_2))) =

x_1_1 %(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2

. ((op sel2 : Data3 ->? Data2) (Cons31 (x_1_1, x_1_2))) =

x_1_2 %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. ((op sel2 : Data3 ->? Data2) (Cons32 (x_1_1, x_1_2))) =

x_1_1 %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. ((op sel1 : Data3 ->? Data1) (Cons32 (x_1_1, x_1_2))) =

x_1_2 %(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

. ((op sel1 : Data4 ->? Data1) (Cons41 (x_1_1, x_1_2))) =

x_1_1 %(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2

. ((op sel2 : Data4 ->? Data2) (Cons41 (x_1_1, x_1_2))) =

x_1_2 %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. ((op sel2 : Data4 ->? Data2) (Cons42 (x_1_1, x_1_2))) =

x_1_1 %(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1

. ((op sel1 : Data4 ->? Data1) (Cons42 (x_1_1, x_1_2))) =

x_1_2 %(ga_select_sel1)%

type Data4

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

Cons42 : Data2 * Data1 ->? Data4

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

true

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

*** Warning 1.7, void universe class declaration 'Type'

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

*** Error 7.11, illegal type pattern argument '__'

*** Error 11.16, not a class 'd'

*** Warning 11.7, unchanged class 'a'

*** Warning 11.10, unchanged class 'b'

*** Warning 11.13, unchanged class 'c'

*** Hint 11.19, refined class 'a'

*** Hint 16.7, not a class 's'

*** Hint 18.15, rebound variable 'x'

*** Error 20.12, unexpected mixfix token: res

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

with (maximal) type: _v4 ->? s

known types:

*** Hint 21.1-21.16, untypable application (with result type: s)

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

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

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

with (maximal) type: _v5 ->? t

known types:

*** Hint 22.1-22.16, untypable application (with result type: t)

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

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

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

with (maximal) type: _v6 ->? ? Unit

known types:

*** Hint 28.9-28.15, untypable application (with result type: ? Unit)

'all (var p : ? s)'

*** Error 28.33, no typing for 'program all (var p : ? s) : ? Unit = eq (p, tt)'

*** Error 30.40, unexpected mixfix token: t1

*** Error 32.12, unexpected mixfix token: impl

*** Error 32.45, unexpected mixfix token: And

*** Error 34.12, unexpected mixfix token: or

*** Error 35.21, unexpected mixfix token: impl

*** Error 34.44, unexpected mixfix token: all

*** Error 38.32, unexpected mixfix token: impl

*** Error 38.17, unexpected mixfix token: all

*** Error 37.27, unexpected mixfix token: all

*** Error 40.20, unexpected mixfix token: all

*** Hint 45.9, not a class 't'

*** Hint 45.8, rebound variable 'x'

*** Hint 45.16, not a class 't'

*** Hint 57.11, redeclared type 's'

*** Hint 66.22, not a class 's'

*** Hint 66.21, rebound variable 'x'

*** Error 66.25, unexpected mixfix token: e

*** Hint 67.9, not a class 's'

*** Hint 67.8, rebound variable 'x'

*** Error 67.12, unexpected mixfix token: e