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) . ()) : s ->? Unit

pred eq : s * s

type s < ? s

forall x : t; y : t

. %(..)%

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

t * t ->? Unit)

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

Unit

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

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 ->? Unit

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

Unit : TYPE

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

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

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

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

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

s : c < ? s

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_v-1 * a_v-1 ->? Unit %(fun)%

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

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

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

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

__when__else__

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

a : Data1 %(construct Data1)%

: ? s %(op)%

b : Data1 %(construct Data1)%

bottom : forall a : Type . a_v-1 %(fun)%

c : Data1 %(construct Data1)%

def__ : forall a : Type . a_v-1 ->? 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)%

x : s %(var)%

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

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

program (pred tt : s) = (\ (var x : s) . ()) : s ->? Unit %(pe_tt)%

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

t * t ->? Unit)

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

Unit

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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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_v-1 * a_v-1 ->? 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'

*** Error, unbound type variable(s)

t : Type in 't_v1'

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

*** Error 11.16, not a 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'

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

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

*** Error 20.12, unexpected mixfix token: res

*** Warning 21.22, trying hard to find lazy type for 'program fst(x : s, var y : t) : s = x'

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

with (maximal) type: _var_4_v4 ->? s

known types:

*** Hint 21.5-21.13, 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'

*** Warning 22.22, trying hard to find lazy type for 'program snd(x : s, var y : t) : t = y'

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

with (maximal) type: _var_5_v5 ->? t

known types:

*** Hint 22.5-22.13, 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 26.6, redeclared type 's'

*** Warning 28.33, trying hard to find lazy type for 'program all(var p : ? s) : ? Unit = eq(p, tt)'

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

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

known types:

*** Hint 28.13-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.16, not a class 't'

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

*** Error 66.25, unexpected mixfix token: e

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

*** Error 67.12, unexpected mixfix token: e