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

Cpo

Flatcpo < Cpo

Pcpo < Cpo

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

? : Type -> Type := \ t : Type . Unit ->? t

?__ : Type -> Type := \ t : Type . Unit ->? t

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

Pred__ : Type- -> Type := \ t : Type- . t ->? Unit

Unit : (Type, Pcpo)

__*__ : (Type+ -> Type+ -> Type, Pcpo+ -> Pcpo+ -> Pcpo,

Cpo+ -> Cpo+ -> Cpo)

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

__-->__ : (Cpo- -> Cpo+ -> Cpo, Cpo- -> Pcpo+ -> Pcpo)

__-->?__ : Cpo- -> Cpo+ -> Pcpo

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

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

bool : (Type, Flatcpo) %[free type __ ::=

true : -> __

false : -> __]%

c : Cpo %(var)%

c-->d : Type < c -->? d

c-->?d : Type < c ->? d

d : Cpo %(var)%

f : Flatcpo %(var)%

nat : (Type, Flatcpo)

p : Pcpo %(var)%

s : Type < ? s %(var)%

s->t : Type < s ->? t

t : Type %(var)%

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

Y : (p -->? p) --> p

__/\__ : Unit � Unit ->? Unit

__<<=__ : c � c ->? Unit

__<=>__ : Unit � Unit ->? Unit

__=__ : s � s ->? Unit

__=>__ : Unit � Unit ->? Unit

__\/__ : Unit � Unit ->? Unit

__if__ : Unit � Unit ->? Unit

__res__ : s = \ (x : s, y : t) .! (op x : s)

bottom : p

def : (Pred)(s) = \ x : s . ()

eq : s � s ->? Unit

f : c --> d %(var)%

false : bool %(construct bool)%

: Unit ->? Unit

fst : s = \ (x : s, y : t) .! (op x : s)

g : c --> d %(var)%

not : Unit ->? Unit

sup : (nat -> c) ->? c

true : bool %(construct bool)%

: Unit ->? Unit

tt : (Pred)(s) = \ x : s . ()

x : s %(var)%

x1 : c %(var)%

x2 : c %(var)%

y1 : d %(var)%

y2 : d %(var)%

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

(op __=__ : s � s ->? Unit) ((op fst : s), (op __res__ : s)) %()%

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

Error (line 4, column 7) illegal universe class declaration 'Type'

Error (line 14, column 44) incompatible kind of: t ->? Unit

expected: Type

found: Type -> Type

Warning (line 15, column 16) redeclared type 't'

Hint (line 40, column 9) not a class 's'

Error (line 46, column 11) unexpected mixfix token 'und'

FatalError (line 54, column 3) no resolution for '__'

Error (line 60, column 13) unexpected mixfix token '('

Error (line 60, column 32) unexpected mixfix token 'y'

Error (line 65, column 22) unexpected mixfix token '('

FatalError (line 65, column 18) no resolution for '(\ (x : s, y : t) . def (x res y)) =

(\ (x : s, y : t) . (def y) und (def x))'

FatalError (line 74, column 11) no resolution for '(\ x : s . eq (x, x)) = tt'

Error (line 75, column 26) unexpected mixfix token 'y'

FatalError (line 75, column 15) no resolution for '(\ (x, y : s) . x res eq (x, y)) = (\ (x, y : s) . y res eq (x, y))'

Warning (line 85, column 6) redeclared type 's'

Error (line 87, column 13) unexpected mixfix token '('

Error (line 87, column 43) unexpected mixfix token 'p'

Error (line 90, column 13) unexpected mixfix token '('

Error (line 90, column 45) unexpected mixfix token 't1'

Error (line 93, column 11) unexpected mixfix token 'impl'

Error (line 93, column 58) unexpected mixfix token 'And'

Error (line 95, column 11) unexpected mixfix token 'or'

Error (line 95, column 48) unexpected mixfix token 'all'

Error (line 96, column 21) unexpected mixfix token 'impl'

Error (line 98, column 12) unexpected mixfix token '('

Error (line 98, column 39) unexpected mixfix token 'all'

Error (line 99, column 17) unexpected mixfix token 'all'

Error (line 99, column 27) unexpected mixfix token 'p'

Error (line 101, column 12) unexpected mixfix token '('

Error (line 101, column 29) unexpected mixfix token 'all'

Error (line 101, column 49) unexpected mixfix token 'r'

Error (line 103, column 13) unexpected mixfix token '('

Error (line 103, column 42) unexpected mixfix token 'r'

Error (line 108, column 3) unexpected mixfix token 'all'

Error (line 108, column 22) unexpected mixfix token 'all'

Error (line 108, column 39) unexpected mixfix token 'f'

FatalError (line 108, column 32) no resolution for 'eq (\ . f (x), g (x)) impl eq (f, g)'

Warning (line 115, column 13) redundant universe class

Error (line 121, column 3) unexpected mixfix token 'all'

FatalError (line 121, column 14) no resolution for 'x <<= x'

Error (line 122, column 3) unexpected mixfix token 'all'

Error (line 122, column 28) unexpected mixfix token 'y'

Error (line 123, column 3) unexpected mixfix token 'all'

Error (line 123, column 28) unexpected mixfix token 'y'

Error (line 125, column 32) unexpected mixfix token 'all'

Error (line 125, column 44) unexpected mixfix token 's'

Error (line 126, column 38) unexpected mixfix token 'all'

Error (line 126, column 50) unexpected mixfix token 's'

Error (line 130, column 3) unexpected mixfix token 'all'

Error (line 130, column 24) unexpected mixfix token '('

Error (line 131, column 42) unexpected mixfix token 'isBound'

Error (line 134, column 3) unexpected mixfix token 'all'

Error (line 134, column 20) unexpected mixfix token 'isChain'

Error (line 143, column 3) unexpected mixfix token 'all'

FatalError (line 143, column 15) no resolution for 'bottom <<= x'

Error (line 150, column 15) unexpected mixfix token '['

Warning (line 153, column 5) redeclared type 'c'

Hint (line 157, column 13) not a class 'c'

Hint (line 157, column 13) not a class 'c'

Hint (line 157, column 25) not a class 'd'

Hint (line 157, column 25) not a class 'd'

FatalError (line 159, column 10) no resolution for '(x1, y1) <<= (x2, y2)'

Error (line 159, column 45) unexpected mixfix token 'und'

FatalError (line 170, column 4) no resolution for '__'

Error (line 176, column 16) unexpected mixfix token '['

Error (line 176, column 31) unexpected mixfix token 'all'

Error (line 176, column 45) unexpected mixfix token '('

FatalError (line 182, column 4) no resolution for '__'

Hint (line 184, column 13) not a class 'c --> d'

Hint (line 184, column 13) not a class 'c --> d'

Error (line 186, column 12) unexpected mixfix token '<<='

Error (line 186, column 22) unexpected mixfix token '<<='

Error (line 192, column 3) unexpected mixfix token 'all'

Error (line 192, column 38) unexpected mixfix token ')'

Error (line 193, column 32) unexpected mixfix token 'impl'

FatalError (line 195, column 27) no resolution for 'Y (\ x : c -->? p .! x)'