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

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

x1 : c %(var)%

x2 : c %(var)%

y1 : d %(var)%

y2 : d %(var)%

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

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

(op __=__ : s � s ->? Unit) (\ x : s . (op eq : s �

s ->? Unit) (((op x : s), (op x : s))),

(op tt : (Pred)(s))) %()%

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

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

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

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

FatalError (line 42, column 1) no analysis yet for: program def = \ x : s . ()

%% def is also total (identical to tt)

FatalError (line 44, column 1) no analysis yet for: program tt = \ x : s . ()

%% tt is total "op tt(x: s): unit = ()"

FatalError (line 46, column 1) no analysis yet for: program __ und __ (x, y : Unit) : Unit = ()

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

FatalError (line 60, column 1) no analysis yet for: program snd (x : s; y : t) : t = y

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

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

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

FatalError (line 87, column 1) no analysis yet for: program all (p : Pred (s)) : Pred Unit = eq (p, tt)

FatalError (line 90, column 1) no analysis yet for: program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()

FatalError (line 93, column 1) no analysis yet for: program __ impl __ (x, y : Pred Unit) : Pred Unit = eq (x, x And y)

FatalError (line 95, column 1) no analysis yet for: program __ or __ (x, y : Pred Unit) : Pred Unit =

all (\ r : Pred Unit . ((x impl r) und (y impl r)) impl r)

FatalError (line 98, column 1) no analysis yet for: program ex (p : Pred (s)) : Pred Unit =

all (\ r : Pred Unit . all (\ x : s . p (x) impl r) impl r)

FatalError (line 101, column 1) no analysis yet for: program ff () : Pred Unit = all (\ r : Pred Unit . r ())

FatalError (line 103, column 1) no analysis yet for: program neg (r : Pred Unit) : Pred Unit = r impl ff

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

Warning (line 115, column 13) redundant universe class

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

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

Error (line 119, column 8) unexpected mixfix token '\ x : c . (op __<<=__ : c � c ->? Unit) ((op x : s), (op x : s))'

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

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

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

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

Error (line 119, column 8) unexpected mixfix token '\ x : p . (op __<<=__ : c � c ->? Unit) ((op bottom : p),

(op x : s))'

FatalError (line 150, column 2) no analysis yet for: program __ <<= [f] __ = eq

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 1) no analysis yet for: program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)

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

FatalError (line 176, column 3) no analysis yet for: program f <<= [c -->? d] g =

all (\ x : c . def (f x) impl f (x) <<= g (x))

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

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

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

FatalError (line 186, column 2) no analysis yet for: program f <<= g = f <<= [c -->? d] g

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

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

Hint (line 17, column 20) type 'bool' is not unifiable with 'Unit ->? Unit'

Hint (line 17, column 20) type 'bool' is not unifiable with 'Unit ->? Unit'