2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashi%% Classes ---------------------------------------------------------------

2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashiCpo

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndFlatcpo < Cpo

dc0d8d65d35787d30a275895ccad8d8e1b58a5edndPcpo < Cpo

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

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

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

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

6aadbc6fd703e73d1d419e9f06b84a4338c898f1maczniakPred__ :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'

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)

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 0, column 0) 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'