Prelude.hascasl.output revision c18e9c3c6d5039618f1f2c05526ece84c7794ea3
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% predefined universe containing all types,
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maeder%% superclass of all other classes
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maederclass Type < Type
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maedervar s : Type; t : Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% invisible type "Unit" for formulae
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder %% flat cpo with bottom
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder %% type aliases
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype Pred : Type- -> Type := \ (t : Type)(t : Type-) . t ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype ? : Type -> Type := \ t : Type . Unit ->? t
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop true, false : Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop __/\__, __\/__, __=>__, __if__, __<=>__ : Unit � Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop not : Unit ->? Unit
335039f3702f6a2584ede16128a00a51fd5b8bf8Jorina Freya Gerkenop : forall s : Type . s � s ->? Unit
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski %% (builtin) type (constructors)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maedertype __ : Type- -> Type+ -> Type
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maeder%% nested pairs are different from n-tupels (n > 2)
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maedertype __ : Type+ -> Type+ -> Type
88c800932dd7053322501ea2039d9f234be6866cKlaus Luettichtype __ : Type+ -> Type+ -> Type+ -> Type
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder%% "pred p args = e" abbreviates "op p args :? unit = e"
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich%% CASL requires "<=>" for pred-defn and disallows "()" as result
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichop def, tt : forall s : Type . s ->? Unit
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichprogram def : forall s : Type . s ->? Unit = \ x : s . ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder %% def is also total (identical to tt)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederprogram tt : forall s : Type . s ->? Unit = \ x : s . ()
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder %% tt is total "op tt(x: s): unit = ()"
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederprogram __ und __ (x, y : Unit) : Unit = ()
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder%% total function type
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maedertype __ : Type- -> Type+ -> Type
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettichtype s < s ->? t
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% total functions
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichop __res__ : s � t ->? s = (var x : s)
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maederop fst : s � t ->? s = (var x : s)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowskiprogram snd (x : s, y : t) : t = y
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich%% trivial because its the strict function property
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder y : t) . def (x res y),
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich \ (x : s, y : t) . (def y) und (def x))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. (op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (op __res__ : s � t ->? s))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich%% Internal Logic
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichop eq : forall s : Type . s � s ->? Unit
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich. (op __=__ : forall a : Type . a �
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich a ->? Unit) (\ x : s . (op eq : forall s : Type . s �
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder s ->? Unit) ((var x : s),
b0294d73dcefc502ddaa13e18b46103a5916971fTill Mossakowski (var x : s)),
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (op tt : forall s : Type . s ->? Unit))
77a65251ee036c6aaf09c2775315a4ee24259fbdJorina Freya Gerken. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x : _var_45,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder y : s) . x res eq (x, y),
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder \ (x : _var_46, y : s) . y res eq (x, y))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% notation "\ ." abbreviates "\bla:unit."
97812b7ce9860bf514a8822a63503451795dbc65Klaus Luettich%% where "bla" is never used, but only "()" instead
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% for type inference
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederprogram all (p : Pred (s)) : Pred Unit = eq (p, tt)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% the cast from ?s to s is still done manually here (for the strict "und")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederprogram And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederprogram __ impl __
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers (x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit
4e7050bcbcf0f372a5bad32ecd0282bccabf0983Klaus Luettich = eq (x, x And y)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederprogram __ or __ (x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich = all (\ r : Pred Unit . ((x impl r) und (y impl r)) impl r)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederprogram ex (p : Pred (s)) : Pred Unit =
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder all (\ r : Pred Unit . all (\ x : s . p (x) impl r) impl r)
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maederprogram ff () : Unit ->? Unit : Unit ->? Unit =
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder all (\ r : Pred Unit . r ())
ce50fe187cdae64e75e510daafb78156280bdb91Christian Maederprogram neg (r : Pred Unit) : Pred Unit = r impl ff
ebe517300051f765f2ed856a789dd5613d681ab0Klaus Luettich%% the type instance for the first "eq" should be "?t"
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers%% this is explicitely enforced by "\ .f(x)"
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederclass Cpo < Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder {var c : Cpo; op __<<=__ : forall c : Cpo . c � c ->? Unit; ;
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder op isChain(s : nat -> c) :? Unit = all
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (\ n : nat . s (n) <<= s (Suc (n)));
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder op isBound(x : c, s : nat -> c) :? Unit = all
ebe517300051f765f2ed856a789dd5613d681ab0Klaus Luettich (\ n : nat . s (n) <<= x);
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers op sup : forall c : Cpo . (nat -> c) ->? c;}
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersclass Pcpo < Cpo
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich {var p : Pcpo; op bottom : forall p : Pcpo . p;}
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederclass instance Flatcpo < Cpo
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder {var f : Flatcpo; program __ <<= [f] __ = eq}
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maedervar c : Cpo; d : Cpo
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maedertype instance __ : Cpo+ -> Cpo+ -> Cpo
ce50fe187cdae64e75e510daafb78156280bdb91Christian Maedervar x1 : c; x2 : c; y1 : d; y2 : d
4e7050bcbcf0f372a5bad32ecd0282bccabf0983Klaus Luettichprogram __<<=__ : forall c : Cpo . c � c ->? Unit ((x1 : _var_75,
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder y1 : _var_76),
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder (x2 : _var_77, y2 : _var_78))
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich = (x1 <<= x2) und (y1 <<= y2)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype instance __ : Pcpo+ -> Pcpo+ -> Pcpo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype Unit : Pcpo
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maedertype instance __ : Cpo- -> Cpo+ -> Pcpo
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckerstype c < c ->? d
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maederprogram f <<= [c -->? d] g =
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder all (\ x : c . def (f x) impl f (x) <<= g (x))
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettichtype instance __ : Cpo- -> Cpo+ -> Cpo
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettichtype c < c -->? d
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maedervar f : c --> d; g : c --> d
c432483b64662e8db604a58758cd18ea7fa65659Christian Maederprogram __<<=__ : forall c : Cpo . c � c ->? Unit (f : _var_103,
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder g : _var_104)
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder = f <<= [c -->? d] g
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maedertype instance __ : Cpo- -> Pcpo+ -> Pcpo
e8d782e6e650b71a2b0ee8461fd8d9fa31525591Christian Maederop Y : forall p : Pcpo . (p -->? p) --> p
0310dabcd02da51f78f84e7a73d4c7b2dd3e8507Christian Maederop undefined : c -->? p = (op Y : forall p : Pcpo . (p -->? p) --> p) (\ x : c -->? p .! (var x : c -->? p))
c5e10ba19c9854112e5d29f491759e8e89f83652Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
88c66e48620750c42b94db9feb01b42ae23dba97Till Mossakowskifree type bool ::= true |
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskitype bool : Flatcpo
8659594bb40eb5f3da5439692f0908300947191eSonja Gröningtype nat : Flatcpo
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder%% Classes ---------------------------------------------------------------
96ef2e46d048c357927f2795a40e9e66f21b85fbSonja Gröning%% Type Constructors -----------------------------------------------------
7d09621f989f5e6dfbf603b36b2fccbacf639a3cTill Mossakowski? : Type -> Type := \ t : Type . Unit ->? t
eeb419aa20c97b4af973e97ee6ae77a8eed29e15Till MossakowskiPred : Type -> Type := \ a : Type . a ->? Unit
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersUnit : Pcpo := Unit
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder__ : (Cpo- -> Pcpo+ -> Pcpo, Cpo- -> Cpo+ -> Cpo,
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers Cpo- -> Cpo+ -> Pcpo, Type- -> Type+ -> Type)
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maederbool : Flatcpo %[free type __ ::=
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder false : -> __]%
7d09621f989f5e6dfbf603b36b2fccbacf639a3cTill Mossakowskic : Cpo < (c -->? d, c ->? d) %(var)%
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskid : Cpo %(var)%
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskif : Flatcpo %(var)%
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersp : Pcpo %(var)%
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeders : Type < (? s, s ->? t) %(var)%
51e836611726885f6d2719d959ed1b51f8fd06f4Klaus Luetticht : Type %(var)%
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski%% Assumptions -----------------------------------------------------------
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskiY : forall p : Pcpo . (p -->? p) --> p
327a9b9bf44b6e33f71fee7526dc1c0035251591Christian Maeder__/\__ : Unit � Unit ->? Unit
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder__<<=__ : forall c : Cpo . c � c ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__<=>__ : Unit � Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__=__ : forall a : Type . a � a ->? Unit
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich__=>__ : Unit � Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__=e=__ : forall a : Type . a � a ->? Unit
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich__\/__ : Unit � Unit ->? Unit
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich__if__ : Unit � Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__res__ : s � t ->? s = \ (x : s, y : t) .! (var x : s)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederbottom : forall p : Pcpo . p
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdef : forall s : Type . s ->? Unit = \ x : s . ()
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maederdef__ : forall a : Type . a ->? Unit
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maedereq : forall s : Type . s � s ->? Unit
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maederf : c --> d %(var)%
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowskifalse : bool %(construct bool)%
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder : Unit ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederfst : s � t ->? s = \ (x : s, y : t) .! (var x : s)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersg : c --> d %(var)%
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maederif__then__else__ : forall a : Type . Unit � a � a ->? a
88c800932dd7053322501ea2039d9f234be6866cKlaus Luettichnot : Unit ->? Unit
ed9207cf24e96b0d6f59985822054ae28cb69b2eChristian Maedernot__ : Unit ->? Unit
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maedersup : forall c : Cpo . (nat -> c) ->? c
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maedertrue : bool %(construct bool)%
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder : Unit ->? Unit
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maedertt : forall s : Type . s ->? Unit = \ x : s . ()
b10267ae0a6523b73113fc2dee9ea628266fce60Christian Maederundefined : c -->? p = (op Y : forall p : Pcpo . (p -->? p) --> p) (\ x : c -->? p .! (var x : c -->? p))
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich%% Sentences -------------------------------------------------------------
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder(op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder y : t) . def (x res y),
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich \ (x : s, y : t) . (def y) und (def x)) %()%
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich(op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich (op __res__ : s � t ->? s)) %()%
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich(op __=__ : forall a : Type . a �
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich a ->? Unit) (\ x : s . (op eq : forall s : Type . s �
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich s ->? Unit) ((var x : s),
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich (var x : s)),
621799f077b3a1ed0f5a35382cfad0602c255b20Klaus Luettich (op tt : forall s : Type . s ->? Unit)) %()%
05a8b581f98b928baca6dab60cd20277659ac760Christian Maeder(op __=__ : forall a : Type . a � a ->? Unit) (\ (x : _var_45,
ed9207cf24e96b0d6f59985822054ae28cb69b2eChristian Maeder y : s) . x res eq (x, y),
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder \ (x : _var_46, y : s) . y res eq (x, y)) %()%
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder%% Diagnostics -----------------------------------------------------------
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 4, column 7) illegal universe class declaration 'Type'
b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaederHint (line 6, column 5) is type variable 's'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederHint (line 6, column 7) is type variable 't'
b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichWarning (line 11, column 6) redeclared type 'Unit'
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus LuettichError (line 14, column 34) incompatible kind of: t
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich expected: Type
f29371d8bd5a232c974e736b06d0d8a655d320fbKlaus LuettichError (line 14, column 44) incompatible kind of: t ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder found: Type -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 14, column 44) incompatible kind of: t ->? Unit
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder found: Type- -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 14, column 6) incompatible kind of: Pred
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder found: Type- -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 22, column 8) wrong type scheme of '__=__'
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich expected: forall a : Type . a � a ->? Unit
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich found: forall s : Type . s � s ->? Unit
b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichError (line 30, column 6) incompatible kind of: __
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type- -> Type+ -> Type
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder found: Type+ -> Type+ -> Type
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederError (line 31, column 6) incompatible kind of: __
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type- -> Type+ -> Type
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder found: Type+ -> Type+ -> Type+ -> Type
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichError (line 46, column 11) unexpected mixfix token: und
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichError (line 46, column 9) unexpected pattern '__ und __ (x, y : Unit)'
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichError (line 46, column 9) illegal toplevel pattern '__ und __ (x, y : Unit)'
5958fabb264ec3f5b2125ac5602121bd34814a79Klaus LuettichWarning (line 50, column 6) redeclared type '__'
5958fabb264ec3f5b2125ac5602121bd34814a79Klaus LuettichWarning (line 52, column 6) redeclared type 's'
e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus LuettichError (line 54, column 3) expected further mixfix token: ["/\\","<=>","=","=>","=e="]
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichError (line 54, column 42) ambiguous mixfix term
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus LuettichError (line 54, column 32) unexpected mixfix token: all
725a68ec81cba9b8aa8647bebfb5baa449803e7eKlaus LuettichError (line 54, column 3) unexpected term '__'
d579f5b263e6c73d466c265f2fbfd45b0e69ca64Klaus LuettichHint (line 0, column 0) type 'Unit' is not unifiable with '_var_13 ->? _var_14'
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederError (line 54, column 16) no type match for '(__=__) (__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 54, column 16) no typing for '(__=__)(__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 60, column 9) no match for 'snd'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 60, column 9) no type match for 'snd (x : s, y : t)'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 60, column 9) no typing for 'snd(x : s, y : t) : t'
438f9bd974c8e668203e636b0f2bc80c589af043Klaus LuettichError (line 65, column 18) ambiguous mixfix term
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder def ((__res__)(x, y))
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (def__)((__res__)(x, y))
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichError (line 65, column 59) unexpected mixfix token: und
4e7050bcbcf0f372a5bad32ecd0282bccabf0983Klaus LuettichError (line 65, column 18) unexpected term 'def (x res y)'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 65, column 52) unexpected term '(def y) und (def x)'
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichError (line 75, column 15) ambiguous mixfix term
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (__res__)(x, eq) (x, y)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (__res__)(x, eq (x, y))
4e7050bcbcf0f372a5bad32ecd0282bccabf0983Klaus LuettichError (line 75, column 44) ambiguous mixfix term
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (__res__)(y, eq) (x, y)
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder (__res__)(y, eq (x, y))
e593b89bfd4952698dc37feced21cefe869d87a2Christian MaederError (line 0, column 0) undeclared type '_var_45'
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaederError (line 75, column 15) unexpected term 'x res eq (x, y)'
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaederError (line 0, column 0) undeclared type '_var_46'
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskiError (line 75, column 44) unexpected term 'y res eq (x, y)'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederWarning (line 85, column 6) redeclared type 's'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 87, column 9) no match for 'all'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 87, column 9) no type match for 'all (p : s ->? Unit)'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 87, column 9) no typing for 'all(p : s ->? Unit) : Unit ->? Unit'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 90, column 9) no match for 'And'
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederError (line 90, column 9) no type match for 'And (x : _var_62, y : Unit ->? Unit)'
94d3aa05411444596b44ede4531f05dd7ac20fdfChristian MaederError (line 90, column 9) no typing for 'And(x : _var_62, y : Unit ->? Unit) : Unit ->? Unit'
dc929508a3bd3c666e9b0182d56898fcafb5d66fChristian MaederError (line 93, column 11) unexpected mixfix token: impl
dc929508a3bd3c666e9b0182d56898fcafb5d66fChristian MaederError (line 93, column 9) unexpected pattern '__ impl __ (x, y : Pred Unit)'
94d3aa05411444596b44ede4531f05dd7ac20fdfChristian MaederError (line 93, column 53) unexpected mixfix token: x
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 95, column 11) unexpected mixfix token: or
8410667510a76409aca9bb24ff0eda0420088274Christian MaederError (line 95, column 9) unexpected pattern '__ or __ (x, y : Pred Unit)'
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian MaederError (line 96, column 19) unexpected mixfix token: x
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian MaederError (line 95, column 48) unexpected mixfix token: all
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian MaederError (line 98, column 9) no match for 'ex'
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian MaederError (line 98, column 9) no type match for 'ex (p : s ->? Unit)'
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian MaederError (line 98, column 9) no typing for 'ex(p : s ->? Unit) : Unit ->? Unit'
8410667510a76409aca9bb24ff0eda0420088274Christian MaederError (line 101, column 13) unexpected mixfix token: )
8410667510a76409aca9bb24ff0eda0420088274Christian MaederError (line 101, column 9) unexpected pattern 'ff ()'
8410667510a76409aca9bb24ff0eda0420088274Christian MaederError (line 101, column 29) unexpected mixfix token: all
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus LuettichError (line 103, column 9) no match for 'neg'
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus LuettichError (line 103, column 9) no type match for 'neg (r : Unit ->? Unit)'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 103, column 9) no typing for 'neg(r : Unit ->? Unit) : Unit ->? Unit'
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 108, column 51) unexpected mixfix token: impl
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 108, column 22) unexpected mixfix token: all
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 108, column 3) unexpected mixfix token: all
ba0ec5e897ef99d420c8c14c2374e0f32b7043dbKlaus LuettichHint (line 117, column 5) is type variable 'c'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 121, column 3) unexpected mixfix token: all
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaederError (line 122, column 31) unexpected mixfix token: und
d17834302eaa101395b4b806cd73670fd864445fChristian MaederError (line 122, column 3) unexpected mixfix token: all
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaederError (line 123, column 31) unexpected mixfix token: und
88c66e48620750c42b94db9feb01b42ae23dba97Till MossakowskiError (line 123, column 3) unexpected mixfix token: all
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till MossakowskiError (line 125, column 55) unexpected mixfix token: Suc
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaederError (line 125, column 32) unexpected mixfix token: all
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederError (line 126, column 50) ambiguous mixfix term
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (__<<=__)(s n, x)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers s ((__<<=__)(n, x))
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 126, column 38) unexpected mixfix token: all
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 131, column 42) unexpected mixfix token: isBound
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus LuettichError (line 130, column 32) unexpected mixfix token: impl
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 130, column 3) unexpected mixfix token: all
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 134, column 20) unexpected mixfix token: isChain
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 134, column 3) unexpected mixfix token: all
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersHint (line 139, column 5) is type variable 'p'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 143, column 3) unexpected mixfix token: all
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till MossakowskiHint (line 148, column 6) is type variable 'f'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 150, column 15) unexpected mixfix token: [
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersHint (line 153, column 5) is type variable 'c'
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaederWarning (line 153, column 5) redeclared type 'c'
88c66e48620750c42b94db9feb01b42ae23dba97Till MossakowskiHint (line 153, column 8) is type variable 'd'
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till MossakowskiError (line 155, column 15) incompatible kind of: __
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers expected: Type- -> Type+ -> Type
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers found: Type+ -> Type+ -> Type
ba0ec5e897ef99d420c8c14c2374e0f32b7043dbKlaus LuettichError (line 0, column 0) undeclared type '_var_75'
ba0ec5e897ef99d420c8c14c2374e0f32b7043dbKlaus LuettichError (line 0, column 0) undeclared type '_var_76'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 0, column 0) undeclared type '_var_77'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 0, column 0) undeclared type '_var_78'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 159, column 45) unexpected mixfix token: und
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 162, column 15) incompatible kind of: __
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder expected: Type- -> Type+ -> Type
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder found: Type+ -> Type+ -> Type
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus LuettichError (line 170, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 171, column 35) unexpected mixfix token: und
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 174, column 45) unexpected mixfix token: +
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 173, column 40) unexpected mixfix token: und
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 172, column 28) unexpected mixfix token: isChain
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersError (line 171, column 9) unexpected mixfix token: all
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 170, column 4) unexpected term '__'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederHint (line 0, column 0) type 'Unit' is not unifiable with '_var_94 ->? _var_95'
d67a33b40578beef2e255a274f89bb9c34aaf056Christian MaederError (line 170, column 20) no type match for '(__=__) (__ in c -->? d,
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski \ f : c ->? d . all
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder (\ (x, y : c) . (def (f x) und x <<= y) impl def (f y)) und all
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder (\ s : nat -> c . (isChain (s) und def f (sup (s))) impl ex
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder (\ m : nat . def f (s (m)) und eq
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder (sup (\ n : nat .! f (s (n + m))),
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder f (sup (s))))))'
ba904a15082557e939db689fcfba0c68c9a4f740Christian MaederError (line 170, column 20) no typing for '(__=__)(__ in c -->? d,
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder \ f : c ->? d . all
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder (\ (x, y : c) . (def (f x) und x <<= y) impl def (f y)) und all
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder (\ s : nat -> c . (isChain (s) und def f (sup (s))) impl ex
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder (\ m : nat . def f (s (m)) und eq
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder (sup (\ n : nat .! f (s (n + m))),
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder f (sup (s))))))'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 176, column 16) unexpected mixfix token: [
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 182, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 182, column 46) ambiguous mixfix term
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 182, column 36) unexpected mixfix token: all
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 182, column 4) unexpected term '__'
75cda7e5b890d050d560d970af244a183f28328fKlaus LuettichHint (line 0, column 0) type 'Unit' is not unifiable with '_var_101 ->? _var_102'
75cda7e5b890d050d560d970af244a183f28328fKlaus LuettichError (line 182, column 18) no type match for '(__=__) (__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 182, column 18) no typing for '(__=__)(__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 0, column 0) undeclared type '_var_103'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 0, column 0) undeclared type '_var_104'
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederError (line 186, column 25) unexpected mixfix token: [
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 193, column 32) unexpected mixfix token: impl
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 192, column 40) unexpected mixfix token: und
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederError (line 192, column 3) unexpected mixfix token: all