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

logical : Type %[free type __ ::=

true : -> __

false : -> __]%

nat : (Type, Flatcpo)

p : Pcpo %(var)%

s : Type < ? s %(var)%

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

t : Type %(var)%

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

1 : Unit %(construct Unit)%

Y : p -->? p --> p

__/\__ : logical � logical -> logical

__<=>__ : logical � logical -> logical

__=__ : s -> s -> logical

__=>__ : logical � logical -> logical

__\/__ : logical � logical -> logical

__if__ : logical � logical -> logical

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

bottom : p

def : (Pred)(s)

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

false : bool %(construct bool)%

: logical %(construct logical)%

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

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

not : logical -> logical

sup : nat -> c ->? c

true : bool %(construct bool)%

: logical %(construct logical)%

tt : (Pred)(s)

x : s %(var)%

x1 : c %(var)%

x2 : c %(var)%

y1 : d %(var)%

y2 : d %(var)%

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

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

Warning (line 13, column 4) repeated value 'true'

Warning (line 13, column 10) repeated value 'false'

Warning (line 27, column 11) redeclared type 'Unit'

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

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

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

%% def is also total (identical to tt)

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

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

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

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

FatalError (line 78, column 1) no analysis yet for: pred eq : s � s

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

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

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

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

FatalError (line 101, 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 104, 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 107, column 1) no analysis yet for: program ff () : Pred Unit = all (\ r : Pred Unit . r ())

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

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

Warning (line 121, column 13) redundant universe class

FatalError (line 125, column 1) no analysis yet for: pred __<<=__ : c � c

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

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

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

FatalError (line 131, column 1) no analysis yet for: pred isChain(s : nat -> c) <=> all

(\ n : nat . s (n) <<= s (Suc (n)))

FatalError (line 132, column 1) no analysis yet for: pred isBound(x : c; s : nat -> c) <=> all (\ n : nat . s (n) <<= x)

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

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

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

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

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

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

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

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

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

FatalError (line 165, column 1) no analysis yet for: program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)

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

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

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

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

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

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

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

Hint (line 11, column 11) type 'bool' is not unifiable with 'logical'

Hint (line 11, column 11) type 'bool' is not unifiable with 'logical'