%% 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 : bool

false : bool]%

c :Cpo %(var)%

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

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

d :Cpo %(var)%

f :Flatcpo %(var)%

logical :Type %[free type __ ::=

true : logical

false : logical]%

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

__=__ : t -> t -> logical

__=>__ : logical � logical -> logical

__\/__ : logical � logical -> logical

__if__ : logical � logical -> logical

bottom : p

def : (Pred)(s)

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

false : bool %(construct bool)%

: logical %(construct logical)%

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

not : logical -> logical

sup : nat -> c ->? c

true : bool %(construct bool)%

: logical %(construct logical)%

tt : (Pred)(s)

undefined : c -->? p = Y (\ x : c -->? p .! x)

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'

Error (line 29, column 5) unexpected mixfix token '='

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 = ()

Error (line 60, column 16) unexpected mixfix token '='

FatalError (line 64, column 1) no analysis yet for: program __ res __ (x : s; y : t) : s = x

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

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

Error (line 72, column 3) unexpected mixfix token 'fst'

Error (line 71, column 3) unexpected mixfix token '('

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

Error (line 81, column 3) unexpected mixfix token '('

Error (line 80, column 3) unexpected mixfix token '('

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)

Error (line 176, column 20) unexpected mixfix token '='

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

Error (line 188, column 18) unexpected mixfix token '='

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'

Error (line 201, column 28) unexpected mixfix token '('

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

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