b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder%% predefined universe containing all types,

d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa%% superclass of all other classes

cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen Kuksaclass Type

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuvars s, t : Type

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder

cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen Kuksa%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder%% invisible type "Unit" for formulae

6d81916b9004f8d9b6032113c5987ab07da47015Karl Luctype Unit

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder %% flat cpo with bottom

d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder%% type aliases

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederpreds true, false : Unit

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederpreds __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Lucpred not : Unit

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederpred __=__ : s * s

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder %% =e=

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc%% (builtin) type (constructors)

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luctype __->?__ : -Type -> +Type -> Type

1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder%% nested pairs are different from n-tupels (n > 2)

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype __*__ : +Type -> +Type -> Type

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% ...

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa%% "pred p args = e" abbreviates "op p args :? unit = e"

b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksa%% CASL requires "<=>" for pred-defn and disallows "()" as result

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaops def, tt : Pred s

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksavar x : s

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucprogram

f6eb05386b068f5968180b21cc225ef0d7d836e7Eugen Kuksadef = \ x : s . ();

1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa%% def is also total (identical to tt)

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederprogram

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maedertt = \ x : s . ();

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

1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa%% total function type

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksatype __->__ : -Type -> +Type -> Type

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype __->__ < __->?__

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% total functions

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucop __res__(x : s; y : t) : s = x;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaop fst(x : s; y : t) : s = x;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaprogram snd (x : s, y : t) : t = y;

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% trivial because its the strict function property

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa. fst = __res__;

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa%% Internal Logic

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucpred eq : s * s

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa. (\ x : s . eq (x, x)) = tt

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa. (\ (x, y : s) . x res eq (x, y))

8b7e9bd07700b2fef4312835be342250347ad849Eugen Kuksa = \ (x, y : s) . y res eq (x, y);

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa%% then %def

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%% notation "\ ." abbreviates "\bla:unit."

8b7e9bd07700b2fef4312835be342250347ad849Eugen Kuksa%% where "bla" is never used, but only "()" instead

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa%% for type inference

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype s < ? s

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% the cast from ?s to s is still done manually here (for the strict "und")

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa%% use "And" instead of "und" to avoid cast from "?unit" to "unit"

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%% the type instance for the first "eq" should be "?t"

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%% this is explicitely enforced by "\ .f(x)"

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen Kuksa%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksatype nat

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaclass Cpo

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc {var c : Cpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa pred __<<=__ : c * c

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksa pred isChain : forall c : Cpo . nat -> c

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa pred isBound : forall c : Cpo . c * (nat -> c)

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc op sup : (nat -> c) ->? c

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc }

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaclass Pcpo < Cpo

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksa {var p : Pcpo

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa op bottom : p

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa }

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaclass instance

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen KuksaFlatcpo < Cpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa{var f : Flatcpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaprogram __ <<=[f] __ = eq;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa}

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksavars c, d : Cpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype instance __*__ : +Cpo -> +Cpo -> Cpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksavars x1, x2 : c; y1, y2 : d

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype instance __*__ : +Pcpo -> +Pcpo -> Pcpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype Unit : Pcpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% Pcont

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype instance __-->?__ : -Cpo -> +Cpo -> Pcpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype __-->?__ < __->?__

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc%% Tcont

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype instance __-->__ : -Cpo -> +Cpo -> Cpo

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksatype __-->__ < __-->?__

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksavars f, g : c --> d

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaprogram f <<= g = f <<=[c -->? d] g;

64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen Kuksatype instance __-->__ : -Cpo -> +Pcpo -> Pcpo

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucfun Y : (p --> p) --> p

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksavars f : p --> p; x : p

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa. f (Y f) = Y f

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa. f x = x => Y f <<= x;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucop undefined : c --> p =

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa Y ((\ x' : c --> p . x') as (c --> p) --> c --> p);

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa%% user stuff

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksafree type bool ::= true | false

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype bool : Flatcpo

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatype nat : Flatcpo

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksaclasses

18741eef977546e24fce1fde1b8a8f817aedc6d0Christian MaederFlatcpo < Type;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen KuksaPcpo < Type

64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen Kuksaclasses

d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen KuksaFlatcpo < Cpo;

befbd45c1a4c171f2194b59016590b02bf4df750Eugen KuksaPcpo < Cpo

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksatypes

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen KuksaUnit : Pcpo;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa__*__ : +Pcpo -> +Pcpo -> Pcpo;

ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksa__-->__ : -Cpo -> +Pcpo -> Pcpo;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa__-->?__ : -Cpo -> +Cpo -> Pcpo;

123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksabool : Flatcpo;

64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen Kuksanat : Flatcpo;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucs : Type

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucvars

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucc : Cpo %(var_249)%;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucd : Cpo %(var_250)%;

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaf : Flatcpo %(var_247)%;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucp : Pcpo %(var_246)%;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luct : Type %(var_2)%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucop Y : forall p : Pcpo . (p --> p) --> p %(fun)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop __<<=__ : forall c : Cpo . c * c ->? Unit %(pred)%

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaop def : forall s : Type . Pred s %(op)%

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksaop eq : forall s : Type . s * s ->? Unit %(pred)%

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaop fst : forall s : Type; t : Type . s * t -> s

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa %[op= \ ((var x : s), (var y : t)) .! (var x : s)]%

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksaop isBound : forall c : Cpo . c * (nat -> c) ->? Unit %(pred)%

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksaop isChain : forall c : Cpo . (nat -> c) ->? Unit %(pred)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop not : Unit ->? Unit %(pred)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop snd : s * t ->? t %(op)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop sup : forall c : Cpo . (nat -> c) ->? c %(op)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop tt : forall s : Type . Pred s %(op)%

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaop undefined : forall p : Pcpo; c : Cpo . c --> p

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa %[op=

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa (fun Y : forall p : Pcpo . (p --> p) --> p)

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa ((\ x' : c --> p . (var x' : c --> p)) as (c --> p) --> c --> p)

18741eef977546e24fce1fde1b8a8f817aedc6d0Christian Maeder as c --> p]%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucvars

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucf : p --> p;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucg : c --> d;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucx : p;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucx1 : c;

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Lucx2 : c;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucy1 : d;

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucy2 : d

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucprogram def = \ x : s . () %(pe_def)%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucprogram tt = \ x : s . () %(pe_tt)%

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Lucforall s : Type; t : Type; x : s; y : t . x res y = (x as s)

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaforall s : Type; t : Type; x : s; y : t . fst (x, y) = (x as s)

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucprogram (var snd : s * t ->? t) (x, y) : t = y %(pe_snd)%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc. fst = __res__

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucforall s : Type . (\ x : s . eq (x, x)) = tt

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksaforall s : Type

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa. (\ (x : s, y : s) . x res eq (x, y))

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa = \ (x : s, y : s) . y res eq (x, y)

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucprogram __ <<=[f] __ = eq %(pe___<<=__)%

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucprogram f <<= g = f <<= g %(pe___<<=__)%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucforall p : Pcpo; f : p --> p . f (Y f) = Y f

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucforall p : Pcpo; f : p --> p; x : p . f x = x => Y f <<= x

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaforall c : Cpo; p : Pcpo

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa. undefined

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc = (Y ((\ x' : c --> p . x') as (c --> p) --> c --> p) as c --> p)

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucfree type bool ::= false | true %(ga_bool)%

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Warning 4.7, void universe class declaration 'Type'

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc### Hint 6.5, is type variable 's'

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa### Hint 6.7, is type variable 't'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Hint 11.6, redeclared type 'Unit'

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc*** Error 14.11, illegal type pattern argument '__'

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa*** Error 15.8, illegal type pattern argument '__'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Warning 17.6,

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksaignoring declaration for builtin identifier 'true'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Warning 17.12,

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksaignoring declaration for builtin identifier 'false'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Warning 19.9,

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksaignoring declaration for builtin identifier '__/\__'

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa### Warning 19.17,

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksaignoring declaration for builtin identifier '__\/__'

dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa### Warning 19.25,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaignoring declaration for builtin identifier '__=>__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Warning 19.33,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaignoring declaration for builtin identifier '__if__'

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc### Warning 19.40,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaignoring declaration for builtin identifier '__<=>__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 22.14,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksano kind found for 's'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa expected: {Cpo}

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa found: {Type}

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 22.14,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksano kind found for 's'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa expected: {Cppo}

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa found: {Type}

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa### Warning 22.8,

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksaignoring declaration for builtin identifier '__=__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 27.8, redeclared type '__->?__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 30.8, redeclared type '__*__'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa*** Error 31.6-31.12, illegal type pattern '__ * __ * __'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 40.7, not a class 's'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 42.16, rebound variable 'x'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 39.14-39.19,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksarepeated declaration of 'def' with type 'Pred s'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 44.15, rebound variable 'x'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 39.14-39.19,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksarepeated declaration of 'tt' with type 'Pred s'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa*** Error 46.11, unexpected mixfix token: und

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 50.8, redeclared type '__->__'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa### Hint 52.8, redeclared type '__->__'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa### Hint 52.18, repeated supertype '__->?__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa*** Error 54.42-54.49,

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksaambiguous mixfix term

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa def (f x)

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa (def f) x

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa*** Error 54.6, unexpected mixfix token: :

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 58.13, rebound variable 'x'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Warning 58.6,

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaignoring declaration for builtin identifier '__res__'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 59.9, rebound variable 'x'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 60.14, rebound variable 'x'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Hint 60.14, rebound variable 'x'

ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa### Warning 60.9-60.26,

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksaillegal lhs pattern

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa'(var snd : s * t ->? t) ((var x : s), (var y : t)) : t'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa*** Error 65.18-65.30,

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederambiguous mixfix term

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder def (x res y)

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder def (x res y)

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa*** Error 65.51-65.69,

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaambiguous mixfix term

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa (def y) und

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc (def y) und

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Hint 65.7, rebound variable 'x'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa*** Error 65.18-65.30, unexpected term 'def (x res y)'

d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa### Hint 65.40, rebound variable 'x'

fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc*** Error 65.51-65.69, unexpected term '(def y) und (def x)'

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder### Hint 65.7, rebound variable 'x'

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder*** Error 65.18-65.30, unexpected term 'def (x res y)'

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder### Hint 65.40, rebound variable 'x'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc*** Error 65.51-65.69, unexpected term '(def y) und (def x)'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc*** Error 65.16,

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksaambiguous typings

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa 1. (\ ((var x : s), (var y : t)) . def (x res y))

8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa= \ ((var x : s), (var y : t)) . (def y) und (def x)

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa 2. (\ ((var x : s), (var y : t)) . def (x res y))

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa= \ ((var x : s), (var y : t)) . (def y) und (def x)

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa*** Error 66.7,

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksain term '(op fst : forall s : Type; t : Type . s * t -> s) = __res__'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa are uninstantiated type variables

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa'[_v46_v38_t, _v47_v37_s]'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 72.11,

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksano kind found for 's'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa expected: {Cpo}

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa found: {Type}

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 72.11,

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederno kind found for 's'

b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maeder expected: {Cppo}

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc found: {Type}

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 74.5, rebound variable 'x'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa### Hint 74.5, rebound variable 'x'

b696e806e85f1c07f2f5ea07f2b5babcd656e0d6Karl Luc### Hint 75.6, rebound variable 'x'

b696e806e85f1c07f2f5ea07f2b5babcd656e0d6Karl Luc### Hint 75.35, rebound variable 'x'

b696e806e85f1c07f2f5ea07f2b5babcd656e0d6Karl Luc### Hint 75.35, rebound variable 'x'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 75.6, rebound variable 'x'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 75.35, rebound variable 'x'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 75.35, rebound variable 'x'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Warning 85.6, new type shadows type variable 's'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 85.11, illegal type variable as supertype 's'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 87.40-87.46,

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksain type of '(pred eq : forall s : Type . s * s)

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa((var p : Pred s), (op tt : forall s : Type . Pred s))'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa typename 'Unit' (72.9)

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa is not unifiable with type 'Unit ->? Unit' (87.33)

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 87.38,

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksano typing for 'program all (p : Pred s) : Pred Unit = eq (p, tt)'

befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa### Hint 90.14, rebound variable 'x'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 90.45, no type found for 't1'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 90.45, untypeable term 't1'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 90.45-90.47, untypeable term 't1 ()'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 90.45-90.50, untypeable term 't1 () und'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 90.45-90.54, untypeable term 't1 () und t2'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 90.43,

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksano typing for

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa'program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 93.11, unexpected mixfix token: impl

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 95.11, unexpected mixfix token: or

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 98.39, no type found for 'all'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 98.39, untypeable term 'all'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 98.37,

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksano typing for

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa'program ex (p : Pred s) : Pred Unit

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa = all \ r : Pred Unit . (all \ x : s . p x impl r) impl r'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 101.29, no type found for 'all'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 101.29, untypeable term 'all'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa*** Error 101.27,

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksano typing for

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa'program ff () : Pred Unit = all \ r : Pred Unit . r ()'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 103.44, no type found for 'impl'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 103.44, untypeable term (with type: Unit) 'impl'

d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa### Hint 103.42-103.44, untypeable term 'r impl'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc*** Error 103.40,

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucno typing for 'program neg (r : Pred Unit) : Pred Unit = r impl ff'

f2bb6f4c9f075b94e7f83a6589f457bc8b7fb30cEugen Kuksa### Hint 108.3, no type found for 'all'

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa### Hint 108.3, untypeable term 'all'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa*** Error 108.3-108.63,

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksano typing for

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa'all

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa \ (f, g) : s ->? t

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc . all \ x : s . eq (\ . f x, g x) impl eq (f, g)'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc### Warning 115.7, unchanged class 'Cpo'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Hint 117.5, is type variable 'c'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc### Hint 119.16,

2aa433939988fc34e3968ae0363fe628374fb3d2Karl Lucno kind found for 'c'

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa expected: {Cppo}

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc found: {Cpo}

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Hint 121.3, no type found for 'all'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc### Hint 121.3, untypeable term 'all'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc*** Error 121.3-121.16, no typing for 'all \ x : c . x <<= x'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc### Hint 122.3, no type found for 'all'

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa### Hint 122.3, untypeable term 'all'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc*** Error 122.3-122.44,

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Lucno typing for

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc'all \ (x, y, z : c) . (x <<= y) und (y <<= z) impl x <<= z'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc### Hint 123.3, no type found for 'all'

18741eef977546e24fce1fde1b8a8f817aedc6d0Christian Maeder### Hint 123.3, untypeable term 'all'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc*** Error 123.3-123.57,

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksano typing for

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc'all \ (x, y, z : c) . (x <<= y) und (y <<= x) impl eq (x, y)'

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa### Hint 125.32, no type found for 'all'

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa### Hint 125.32, untypeable term 'all'

823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc*** Error 125.14-125.46,

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucno typing for '(all \ n : nat . s n <<= s (Suc n)) as Unit'

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa### Hint 126.15, rebound variable 'x'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 126.38, no type found for 'all'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 126.38, untypeable term 'all'

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa*** Error 126.14-126.52,

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucno typing for '(all \ n : nat . s n <<= x) as Unit'

07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc*** Error 130.21-131.74,

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksaambiguous mixfix term

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa def (((sup s) impl)

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa ((((isBound (sup s, s)) und) all)

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x)))

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa ((def (sup s)) impl)

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa((((isBound (sup s, s)) und) all)

cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x))

08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa### Hint 130.3, no type found for 'all'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 130.3, untypeable term 'all'

c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc*** Error 130.3-131.74,

1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksano typing for

0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa'all

\ s : nat -> c

. def (sup s) impl

(isBound (sup s, s) und all

(\ x : c . isBound (x, s) impl sup (s) <<= x))'

### Hint 134.3, no type found for 'all'

### Hint 134.3, untypeable term 'all'

*** Error 134.3-134.46,

no typing for 'all \ s : nat -> c . isChain s impl def (sup s)'

### Hint 139.5, is type variable 'p'

### Warning 141.4,

ignoring declaration for builtin identifier 'bottom'

### Hint 143.3, no type found for 'all'

### Hint 143.3, untypeable term 'all'

*** Error 143.3-143.22, no typing for 'all \ x : p . bottom <<= x'

### Hint 148.6, is type variable 'f'

### Hint 150.15-150.17, is type list '[f]'

### Hint 119.14-119.18,

repeated declaration of '__<<=__' with type 'c * c ->? Unit'

### Hint 153.5, is type variable 'c'

### Hint 153.5, rebound type variable 'c'

### Hint 153.8, is type variable 'd'

### Hint 155.17, redeclared type '__*__'

### Hint 157.7, not a class 'c'

### Hint 157.11, not a class 'c'

### Hint 157.18, not a class 'd'

### Hint 157.23, not a class 'd'

### Hint 159.10, rebound variable 'x1'

### Hint 159.14, rebound variable 'y1'

### Hint 159.23, rebound variable 'x2'

### Hint 159.27, rebound variable 'y2'

### Hint 159.33-159.45, untypeable term '(x1 <<= x2) und'

*** Error 159.31,

no typing for

'program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)'

### Hint 169.9, redeclared type '__-->?__'

### Hint 169.20, repeated supertype '__->?__'

*** Error 171.24-171.61,

ambiguous mixfix term

(def (((f x) und) x)) <<= y

(((def (f x)) und) x) <<= y

*** Error 174.45, unexpected mixfix token: +

*** Error 173.28-174.61,

ambiguous mixfix term

def ((((f (s m)) und) eq)

(sup (\ n : nat .! f (s (n + m))), f (sup s)))

((((def f) (s m)) und) eq)

(sup (\ n : nat .! f (s (n + m))), f (sup s))

*** Error 170.7, unexpected mixfix token: :

### Hint 176.16-176.25, is type list '[c -->? d]'

*** Error 176.41-176.68,

ambiguous mixfix term

(def ((((f x) impl) f) x)) <<= (g x)

((((def (f x)) impl) f) x) <<= (g x)

### Warning 176.11, variable also known as type variable 'f'

### Hint 176.31, no type found for 'all'

### Hint 176.31, untypeable term 'all'

*** Error 176.29,

no typing for

'program f <<=[c -->? d] g

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

### Hint 179.17, redeclared type '__-->__'

### Warning 181.17-181.23, non-unique kind for '__ -->? __'

### Hint 181.9, redeclared type '__-->__'

### Hint 181.19, repeated supertype '__-->?__'

### Hint 182.16,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

*** Error 182.46-182.53,

ambiguous mixfix term

def (f x)

(def f) x

*** Error 182.7, unexpected mixfix token: :

### Hint 184.7, not a kind 'c --> d'

### Hint 184.19,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

### Warning 184.6, variable also known as type variable 'f'

### Hint 184.11, not a kind 'c --> d'

### Hint 184.19,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

### Hint 186.25-186.34, is type list '[c -->? d]'

### Hint 186.10, rebound variable 'f'

### Warning 186.10, variable also known as type variable 'f'

### Hint 186.16, rebound variable 'g'

### Hint 186.10, rebound variable 'f'

### Warning 186.10, variable also known as type variable 'f'

### Hint 186.16, rebound variable 'g'

### Hint 119.14-119.18,

repeated declaration of '__<<=__' with type 'c * c ->? Unit'

### Hint 190.16,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 190.23,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 192.3, no type found for 'all'

### Hint 192.3, untypeable term 'all'

*** Error 192.3-193.47,

no typing for

'all

\ f : p -->? p

. eq (f (Y f), Y f) und all \ x : p . eq (f x, x) impl Y f <<= x'

### Hint 195.7, not a kind 'p --> p'

### Hint 195.15,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 195.5, rebound variable 'f'

### Warning 195.5, variable also known as type variable 'f'

### Hint 195.20, not a class 'p'

### Hint 195.18, rebound variable 'x'

### Hint 199.22,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.40,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.58,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.71,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.65-199.71,

no kind found for 'c --> p'

expected: {Cppo}

found: {Pcpo}

### Warning 204.20,

ignoring declaration for builtin identifier 'true'

### Warning 204.27,

ignoring declaration for builtin identifier 'false'