967e5f3c25249c779575864692935627004d3f9eChristian Maeder%% predefined universe containing all types,

967e5f3c25249c779575864692935627004d3f9eChristian Maeder%% superclass of all other classes

81d182b21020b815887e9057959228546cf61b6bChristian Maederclass Type

f11f713bebd8e1e623a0a4361065df256033de47Christian Maedervar s : Type; t : Type

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

967e5f3c25249c779575864692935627004d3f9eChristian Maeder%% invisible type "Unit" for formulae

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maedertype Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maeder %% flat cpo with bottom

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder %% type aliases

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedertype Pred : Type- -> Type := \ (t : Type)(t : Type-) . t ->? Unit

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedertype ? : Type -> Type := \ t : Type . Unit ->? t

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederop true, false : Unit ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maederop __/\__, __\/__, __=>__, __if__, __<=>__ : Unit � Unit ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maederop not : Unit ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maederop : forall s : Type . s � s ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maeder %% =e=

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder %% (builtin) type (constructors)

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype __ : Type- -> Type+ -> Type

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

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype __ : Type+ -> Type+ -> Type

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maedertype __ : Type+ -> Type+ -> Type+ -> Type

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder%% ...

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder%% "pred p args = e" abbreviates "op p args :? unit = e"

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

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederop def, tt : forall s : Type . s ->? Unit

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maedervar x : s

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederprogram def = \ x : s . ()

967e5f3c25249c779575864692935627004d3f9eChristian Maeder %% def is also total (identical to tt)

8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maederprogram tt = \ x : s . ()

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

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederprogram __ und __ (x, y : Unit) : Unit = ()

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder%% total function type

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maedertype __ : Type- -> Type+ -> Type

ad187062b0009820118c1b773a232e29b879a2faChristian Maedertype s < s ->? t

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder%% total functions

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederop __res__ : s � t ->? s = (var x : s)

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederop fst : s � t ->? s = (var x : s)

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederprogram snd(x : s, y : t) : t = (var y : t)

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder%% trivial because its the strict function property

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s : s,

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder y : t) . def (x res y),

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder \ (x : s : s, y : t) . (def y) und (def x))

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder. (op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder t ->? s),

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (op __res__ : s � t ->? s))

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder%% Internal Logic

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederop eq : forall s : Type . s � s ->? Unit

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder. (op __=__ : forall a : Type . a �

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder a ->? Unit) (\ x : s : s . (op eq : forall s : Type . s �

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder s ->? Unit) ((var x : s),

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (var x : s)),

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (op tt : forall s : Type . s ->? Unit))

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder y : s) . x res eq (x, y),

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder \ (x : s, y : s) . y res eq (x, y))

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%% then %def

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%% notation "\ ." abbreviates "\bla:unit."

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%% where "bla" is never used, but only "()" instead

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%% for type inference

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maedertype s < ? s

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederprogram all(p : s ->? Unit) : Unit ->? Unit =

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (op eq : forall s : Type . s � s ->? Unit) ((var p : s ->? Unit),

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (op tt : forall s : Type . s ->? Unit))

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder%% the cast from ?s to s is still done manually here (for the strict "und")

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederprogram And(x : _var_61, y : Unit ->? Unit) : Unit ->? Unit =

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder t1 () und t2 ()

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder%% use "And" instead of "und" to avoid cast from "?unit" to "unit"

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederprogram __ impl __

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder = eq (x, x And y)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederprogram __ or __ (x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder = all (\ r : Pred Unit . ((x impl r) und (y impl r)) impl r)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederprogram ex(p : s ->? Unit) : Unit ->? Unit =

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

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maederprogram ff () : Unit ->? Unit : Unit ->? Unit =

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder all (\ r : Pred Unit . r ())

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederprogram neg(r : Unit ->? Unit) : Unit ->? Unit = r impl ff

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder%% the type instance for the first "eq" should be "?t"

a89389521ddf76109168a0b339031575aafbd512Christian Maeder%% this is explicitely enforced by "\ .f(x)"

a89389521ddf76109168a0b339031575aafbd512Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

a89389521ddf76109168a0b339031575aafbd512Christian Maeder%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"

a89389521ddf76109168a0b339031575aafbd512Christian Maedertype nat

a89389521ddf76109168a0b339031575aafbd512Christian Maederclass Cpo < Type

a89389521ddf76109168a0b339031575aafbd512Christian Maeder {var c : Cpo; op __<<=__ : forall c : Cpo . c � c ->? Unit; ;

a89389521ddf76109168a0b339031575aafbd512Christian Maeder op isChain(s : nat -> c) :? Unit = all

a89389521ddf76109168a0b339031575aafbd512Christian Maeder (\ n : nat . s (n) <<= s (Suc (n)));

a89389521ddf76109168a0b339031575aafbd512Christian Maeder op isBound(x : c, s : nat -> c) :? Unit = all

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder (\ n : nat . s (n) <<= x);

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder op sup : forall c : Cpo . (nat -> c) ->? c;}

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederclass Pcpo < Cpo

9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder {var p : Pcpo; op bottom : forall p : Pcpo . p;}

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederclass instance Flatcpo < Cpo

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder {var f : Flatcpo; program __ <<= [f] __ = eq}

67d92da5e9610aabad39055a16031154b4dc3748Christian Maedervar c : Cpo; d : Cpo

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maedertype instance __ : Cpo+ -> Cpo+ -> Cpo

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedervar x1 : c; x2 : c; y1 : d; y2 : d

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederprogram (__<<=__)((x1 : _var_66, y1 : _var_67),

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder (x2 : _var_68, y2 : _var_69))

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder = (x1 <<= x2) und (y1 <<= y2)

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype instance __ : Pcpo+ -> Pcpo+ -> Pcpo

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype Unit : Pcpo

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder%% Pcont

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype instance __ : Cpo- -> Cpo+ -> Pcpo

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype c < c ->? d

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maederprogram f <<= [c -->? d] g =

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

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder%% Tcont

67d92da5e9610aabad39055a16031154b4dc3748Christian Maedertype instance __ : Cpo- -> Cpo+ -> Cpo

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maedertype c < c -->? d

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedervar f : c --> d; g : c --> d

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maederprogram (__<<=__)(f : _var_85, g : _var_86) = f <<= [c -->? d] g

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedertype instance __ : Cpo- -> Pcpo+ -> Pcpo

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maederop Y : forall p : Pcpo . (p -->? p) --> p

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maederop undefined : c -->? p = (op Y : forall p : Pcpo . (p -->? p) --> p) (\ x : c -->? p .! (var x : c -->? p))

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder%% user stuff

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maederfree type bool ::= true |

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder false

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedertype bool : Flatcpo

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedertype nat : Flatcpo

d48085f765fca838c1d972d2123601997174583dChristian Maeder%% Classes ---------------------------------------------------------------

d48085f765fca838c1d972d2123601997174583dChristian MaederCpo

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederFlatcpo < Cpo

d48085f765fca838c1d972d2123601997174583dChristian MaederPcpo < Cpo

d48085f765fca838c1d972d2123601997174583dChristian Maeder%% Type Constructors -----------------------------------------------------

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder? : Type -> Type := \ t : Type . Unit ->? t

d48085f765fca838c1d972d2123601997174583dChristian MaederPred : (Type -> Type, Type- -> Type) := \ a : Type . a ->? Unit

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederUnit : (Type, Pcpo) := Unit

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder__ : (Type- -> Type+ -> Type, Cpo- -> Pcpo+ -> Pcpo,

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Cpo- -> Cpo+ -> Cpo, Cpo- -> Cpo+ -> Pcpo, Pcpo+ -> Pcpo+ -> Pcpo,

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder Cpo+ -> Cpo+ -> Cpo, Type+ -> Type+ -> Type+ -> Type,

9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder Type+ -> Type+ -> Type)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maederbool : (Type, Flatcpo) %[free type __ ::=

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder true : -> __

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder false : -> __]%

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederc : (Cpo, Type) < (c -->? d, c ->? d) %(var)%

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maederd : Cpo %(var)%

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederf : Flatcpo %(var)%

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maedernat : (Type, Flatcpo)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maederp : Pcpo %(var)%

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeders : Type < (? s, s ->? t) %(var)%

67d92da5e9610aabad39055a16031154b4dc3748Christian Maedert : Type %(var)%

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder%% Assumptions -----------------------------------------------------------

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederY : forall p : Pcpo . (p -->? p) --> p

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder__/\__ : Unit � Unit ->? Unit

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder__<<=__ : forall c : Cpo . c � c ->? Unit

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder__<=>__ : Unit � Unit ->? Unit

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder__=__ : forall a : Type . a � a ->? Unit

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder__=>__ : Unit � Unit ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maeder__=e=__ : forall a : Type . a � a ->? Unit

18b513ff41708f24e1a7407f36b719add813ffeaChristian Maeder__\/__ : Unit � Unit ->? Unit

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder__if__ : Unit � Unit ->? Unit

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder__res__ : s � t ->? s = \ (x : s, y : t) .! (var x : s)

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maederbottom : forall p : Pcpo . p

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maederdef : forall s : Type . s ->? Unit

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maederdef__ : forall a : Type . a ->? Unit

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maedereq : forall s : Type . s � s ->? Unit

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maederf : c --> d %(var)%

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescufalse : bool %(construct bool)%

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder : Unit ->? Unit

81d182b21020b815887e9057959228546cf61b6bChristian Maederfst : s � t ->? s = \ (x : s, y : t) .! (var x : s)

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maederg : c --> d %(var)%

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maederif__then__else__ : forall a : Type . Unit � a � a ->? a

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maedernot : Unit ->? Unit

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maedernot__ : Unit ->? Unit

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maedersup : forall c : Cpo . (nat -> c) ->? c

d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maedertrue : bool %(construct bool)%

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder : Unit ->? Unit

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maedertt : forall s : Type . s ->? Unit

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederundefined : c -->? p = (op Y : forall p : Pcpo . (p -->? p) --> p) (\ x : c -->? p .! (var x : c -->? p))

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder%% Sentences -------------------------------------------------------------

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder(op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s : s,

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder y : t) . def (x res y),

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder \ (x : s : s, y : t) . (def y) und (def x)) %()%

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder(op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder t ->? s),

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder (op __res__ : s � t ->? s)) %()%

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder(op __=__ : forall a : Type . a �

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder a ->? Unit) (\ x : s : s . (op eq : forall s : Type . s �

c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder s ->? Unit) ((var x : s),

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder (var x : s)),

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (op tt : forall s : Type . s ->? Unit)) %()%

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder(op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder y : s) . x res eq (x, y),

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder \ (x : s, y : s) . y res eq (x, y)) %()%

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder%% Diagnostics -----------------------------------------------------------

842eedc62639561781b6c33533d1949693ef6cc5Christian MaederError (line 4, column 7) illegal universe class declaration 'Type'

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiHint (line 6, column 5) is type variable 's'

967e5f3c25249c779575864692935627004d3f9eChristian MaederHint (line 6, column 7) is type variable 't'

967e5f3c25249c779575864692935627004d3f9eChristian MaederWarning (line 11, column 6) redeclared type 'Unit'

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai CodescuError (line 14, column 44) incompatible kind of: t ->? Unit

967e5f3c25249c779575864692935627004d3f9eChristian Maeder expected: Type

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder found: Type -> Type

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederWarning (line 15, column 16) redeclared type 't'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 22, column 8) wrong type scheme of '__=__'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder expected: forall a : Type . a � a ->? Unit

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder found: forall s : Type . s � s ->? Unit

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 31, column 6) incompatible kind of: __

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder expected: Type -> Type -> Type -> Type

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder found: Type -> Type -> Type

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 46, column 11) unexpected mixfix token: und

967e5f3c25249c779575864692935627004d3f9eChristian MaederError (line 46, column 9) no toplevel pattern '__ und __ (x, y : Unit) : Unit : Unit'

967e5f3c25249c779575864692935627004d3f9eChristian MaederWarning (line 50, column 6) redeclared type '__'

ad187062b0009820118c1b773a232e29b879a2faChristian MaederWarning (line 52, column 6) redeclared type 's'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 3) expected further mixfix token: ["/\\","<=>","=","=>","=e="]

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 42) ambiguous mixfix term

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder def f x

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (def__)(f) x

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 32) unexpected mixfix token: all

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 3) unexpected term '__'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederHint (line 0, column 0) type 'Unit' is not unifiable with '_var_10 ->? _var_11'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 16) no type match for '(__=__) (__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 54, column 16) no typing for '(__=__)(__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 65, column 18) ambiguous mixfix term

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder def ((__res__)(x, y))

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (def__)((__res__)(x, y))

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 65, column 59) unexpected mixfix token: und

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 65, column 18) unexpected term 'def (x res y)'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 65, column 52) unexpected term '(def y) und (def x)'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 75, column 15) ambiguous mixfix term

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (__res__)(x, eq (x, y))

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (__res__)(x, eq) (x, y)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 75, column 44) ambiguous mixfix term

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (__res__)(y, eq (x, y))

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (__res__)(y, eq) (x, y)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 75, column 15) unexpected term 'x res eq (x, y)'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 75, column 44) unexpected term 'y res eq (x, y)'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederWarning (line 85, column 6) redeclared type 's'

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 90, column 45) unexpected mixfix token: t1

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 93, column 11) unexpected mixfix token: impl

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 93, column 53) unexpected mixfix token: x

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 95, column 11) unexpected mixfix token: or

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 96, column 19) unexpected mixfix token: x

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 95, column 48) unexpected mixfix token: all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 99, column 32) unexpected mixfix token: impl

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 99, column 17) unexpected mixfix token: all

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 98, column 39) unexpected mixfix token: all

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 101, column 13) unexpected mixfix token: )

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 101, column 29) unexpected mixfix token: all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 103, column 44) unexpected mixfix token: impl

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 108, column 51) unexpected mixfix token: impl

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 108, column 22) unexpected mixfix token: all

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 108, column 3) unexpected mixfix token: all

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederWarning (line 115, column 13) redundant universe class

9659c509ce5e78adc51d7b02a76274eddcba9338Christian MaederHint (line 117, column 5) is type variable 'c'

9659c509ce5e78adc51d7b02a76274eddcba9338Christian MaederError (line 121, column 3) unexpected mixfix token: all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 122, column 31) unexpected mixfix token: und

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 122, column 3) unexpected mixfix token: all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 123, column 31) unexpected mixfix token: und

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 123, column 3) unexpected mixfix token: all

9659c509ce5e78adc51d7b02a76274eddcba9338Christian MaederError (line 125, column 55) unexpected mixfix token: Suc

9659c509ce5e78adc51d7b02a76274eddcba9338Christian MaederError (line 125, column 32) unexpected mixfix token: all

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian MaederError (line 126, column 50) ambiguous mixfix term

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder s ((__<<=__)(n, x))

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (__<<=__)(s n, x)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 126, column 38) unexpected mixfix token: all

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 131, column 42) unexpected mixfix token: isBound

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederError (line 130, column 32) unexpected mixfix token: impl

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederError (line 130, column 3) unexpected mixfix token: all

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederError (line 134, column 20) unexpected mixfix token: isChain

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaederError (line 134, column 3) unexpected mixfix token: all

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaederHint (line 139, column 5) is type variable 'p'

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederError (line 143, column 3) unexpected mixfix token: all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederHint (line 148, column 6) is type variable 'f'

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederError (line 150, column 15) unexpected mixfix token: [

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederHint (line 153, column 5) is type variable 'c'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederWarning (line 153, column 5) redeclared type 'c'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederHint (line 153, column 8) is type variable 'd'

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 159, column 45) unexpected mixfix token: und

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 170, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederError (line 171, column 35) unexpected mixfix token: und

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederError (line 174, column 45) unexpected mixfix token: +

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederError (line 173, column 40) unexpected mixfix token: und

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederError (line 172, column 28) unexpected mixfix token: isChain

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaederError (line 171, column 9) unexpected mixfix token: all

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederError (line 170, column 4) unexpected term '__'

ad187062b0009820118c1b773a232e29b879a2faChristian MaederHint (line 0, column 0) type 'Unit' is not unifiable with '_var_76 ->? _var_77'

ad187062b0009820118c1b773a232e29b879a2faChristian MaederError (line 170, column 20) no type match for '(__=__) (__ in c -->? d,

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder \ f : c ->? d . all

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (\ (x, y : c) . (def (f x) und x <<= y) impl def (f y)) und all

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder (\ s : nat -> c . (isChain (s) und def f (sup (s))) impl ex

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder (\ m : nat . def f (s (m)) und eq

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

f (sup (s))))))'

Error (line 170, column 20) no typing for '(__=__)(__ in c -->? d,

\ f : c ->? d . all

(\ (x, y : c) . (def (f x) und x <<= y) impl def (f y)) und all

(\ s : nat -> c . (isChain (s) und def f (sup (s))) impl ex

(\ m : nat . def f (s (m)) und eq

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

f (sup (s))))))'

Error (line 176, column 16) unexpected mixfix token: [

Warning (line 181, column 7) redeclared type 'c'

Error (line 182, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

Error (line 182, column 46) ambiguous mixfix term

def f x

(def__)(f) x

Error (line 182, column 36) unexpected mixfix token: all

Error (line 182, column 4) unexpected term '__'

Hint (line 0, column 0) type 'Unit' is not unifiable with '_var_83 ->? _var_84'

Error (line 182, column 18) no type match for '(__=__) (__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'

Error (line 182, column 18) no typing for '(__=__)(__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'

Error (line 186, column 25) unexpected mixfix token: [

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

Error (line 192, column 40) unexpected mixfix token: und

Error (line 192, column 3) unexpected mixfix token: all