Prelude.hascasl.output revision c4280f2006756af8b2c102e390e5c46c9c1a612f
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sievers%% predefined universe containing all types,
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sievers%% superclass of all other classes
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringvars s, t : Type
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers%% invisible type "Unit" for formulae
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering %% flat cpo with bottom
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering%% type aliases
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sieverspreds true, false : Unit
7bcd865d386d96caac83cb1c589fdb8f9ce3b081Zbigniew Jędrzejewski-Szmekpreds __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit
7bcd865d386d96caac83cb1c589fdb8f9ce3b081Zbigniew Jędrzejewski-Szmekpred __=__ : s * s
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sievers%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2f8d077ece024b985f2501dc8c904c2d29967acbKay Sievers%% (builtin) type (constructors)
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringtype __->?__ : -Type -> +Type -> Type
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering%% nested pairs are different from n-tupels (n > 2)
c0fe5db522b52f27e030655ce2c03e05cbbc1558Kay Sieverstype __*__ : +Type -> +Type -> Type
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sievers%% "pred p args = e" abbreviates "op p args :? unit = e"
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sievers%% CASL requires "<=>" for pred-defn and disallows "()" as result
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poetteringops def, tt : Pred s
0028da22f194f7c0ca7169a48cf32e1bc0f9138aLennart Poetteringdef = \ x : s . ();
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering%% def is also total (identical to tt)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtt = \ x : s . ();
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering%% tt is total "op tt(x: s): unit = ()"
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering%% total function type
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poetteringtype __->__ : -Type -> +Type -> Type
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poetteringtype __->__ < __->?__
788f75a0e766738c052086e856b7c1b1b676de6bLennart Poettering%% total functions
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop __res__(x : s; y : t) : s = x;
205b7fa46594b38901636b167b02a8725d915b79Lennart Poetteringop fst(x : s; y : t) : s = x;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram snd (x : s, y : t) : t = y;
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering%% trivial because its the strict function property
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering. fst = __res__;
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering%% Internal Logic
990ffbe5cffe7f11a8d3ab2258a85fc52b97bf60Lennart Poetteringpred eq : s * s
dd359de89b1fbabf6f4eb5003d2b5a806b6185c1Lennart Poettering. (\ x : s . eq (x, x)) = tt
dd359de89b1fbabf6f4eb5003d2b5a806b6185c1Lennart Poettering. (\ (x, y : s) . x res eq (x, y))
dd359de89b1fbabf6f4eb5003d2b5a806b6185c1Lennart Poettering = \ (x, y : s) . y res eq (x, y);
dd359de89b1fbabf6f4eb5003d2b5a806b6185c1Lennart Poettering%% notation "\ ." abbreviates "\bla:unit."
dd359de89b1fbabf6f4eb5003d2b5a806b6185c1Lennart Poettering%% where "bla" is never used, but only "()" instead
d01a73b6396f57792113c1b5df6e8492fc703e5eLennart Poettering%% for type inference
d01a73b6396f57792113c1b5df6e8492fc703e5eLennart Poettering%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
990ffbe5cffe7f11a8d3ab2258a85fc52b97bf60Lennart Poettering%% the cast from ?s to s is still done manually here (for the strict "und")
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering%% the type instance for the first "eq" should be "?t"
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering%% this is explicitely enforced by "\ .f(x)"
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering pred __<<=__ : c * c
5965984d6b9f7751d6281028142ecf3ca475f156Lennart Poettering pred isChain : forall c : Cpo . nat -> c
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering pred isBound : forall c : Cpo . c * (nat -> c)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering op sup : (nat -> c) ->? c
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringclass Pcpo < Cpo
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering{var f : Flatcpo
c0fe5db522b52f27e030655ce2c03e05cbbc1558Kay Sieversprogram __ <<=[f] __ = eq;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringvars c, d : Cpo
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poetteringtype instance __*__ : +Cpo -> +Cpo -> Cpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringvars x1, x2 : c; y1, y2 : d
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype instance __*__ : +Pcpo -> +Pcpo -> Pcpo
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poetteringtype Unit : Pcpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype instance __-->?__ : -Cpo -> +Cpo -> Pcpo
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poetteringtype __-->?__ < __->?__
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype instance __-->__ : -Cpo -> +Cpo -> Cpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype __-->__ < __-->?__
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringvars f, g : c --> d
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram f <<= g = f <<=[c -->? d] g;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype instance __-->__ : -Cpo -> +Pcpo -> Pcpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringfun Y : (p --> p) --> p
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringvars f : p --> p; x : p
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering. f (Y f) = Y f
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering. f x = x => Y f <<= x;
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringop undefined : c --> p =
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering Y ((\ x' : c --> p . x') as (c --> p) --> c --> p);
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringfree type bool ::= true | false
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringtype bool : Flatcpo
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poetteringtype nat : Flatcpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringFlatcpo < Type;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering__*__ : +Pcpo -> +Pcpo -> Pcpo;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering__-->__ : -Cpo -> +Pcpo -> Pcpo;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering__-->?__ : -Cpo -> +Cpo -> Pcpo;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringbool : Flatcpo;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringc : Cpo %(var_465)%;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringd : Cpo %(var_466)%;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringf : Flatcpo %(var_463)%;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringp : Pcpo %(var_461)%;
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringt : Type %(var_2)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop Y : forall p : Pcpo . (p --> p) --> p %(fun)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop __<<=__ : forall c : Cpo . c * c ->? Unit %(pred)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop def : forall s : Type . Pred s %(op)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop eq : forall s : Type . s * s ->? Unit %(pred)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop fst : forall s : Type; t : Type . s * t -> s
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering %[op= \ ((var x : s), (var y : t)) .! (var x : s)]%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop isBound : forall c : Cpo . c * (nat -> c) ->? Unit %(pred)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop isChain : forall c : Cpo . (nat -> c) ->? Unit %(pred)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop not : Unit ->? Unit %(pred)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop snd : s * t ->? t %(op)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop sup : forall c : Cpo . (nat -> c) ->? c %(op)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop tt : forall s : Type . Pred s %(op)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringop undefined : forall p : Pcpo; c : Cpo . c --> p
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering (fun Y : forall p : Pcpo . (p --> p) --> p)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering ((\ x' : c --> p . (var x' : c --> p)) as (c --> p) --> c --> p)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram def = \ x : s . () %(pe_def)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram tt = \ x : s . () %(pe_tt)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall s : Type; t : Type; x : s; y : t . x res y = (x as s)
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringforall s : Type; t : Type; x : s; y : t . fst (x, y) = (x as s)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering. fst = __res__
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall s : Type . (\ x : s . eq (x, x)) = tt
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall s : Type
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering. (\ (x : s, y : s) . x res eq (x, y))
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering = \ (x : s, y : s) . y res eq (x, y)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram __ <<=[f] __ = eq %(pe___<<=__)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringprogram f <<= g = f <<= g %(pe___<<=__)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall p : Pcpo; f : p --> p . f (Y f) = Y f
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall p : Pcpo; f : p --> p; x : p . f x = x => Y f <<= x
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringforall c : Cpo; p : Pcpo
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering = (Y ((\ x' : c --> p . x') as (c --> p) --> c --> p) as c --> p)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringfree type bool ::= false | true %(ga_bool)%
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 4.7, void universe class declaration 'Type'
8b04b925e587ff56568c62ff5ad3f2ea2b34ca7aLennart Poettering### Hint 6.5, is type variable 's'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 6.7, is type variable 't'
7361c3b4e1e28a7eb4354a3da354b22e79782141Lennart Poettering### Hint 11.6, redeclared type 'Unit'
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering*** Error 14.11, illegal type pattern argument '__'
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering*** Error 15.8, illegal type pattern argument '__'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 17.6,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringignoring declaration for builtin identifier 'true'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 17.12,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringignoring declaration for builtin identifier 'false'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 19.9,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringignoring declaration for builtin identifier '__/\__'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 19.17,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringignoring declaration for builtin identifier '__\/__'
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering### Warning 19.25,
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sieversignoring declaration for builtin identifier '__=>__'
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers### Warning 19.33,
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sieversignoring declaration for builtin identifier '__if__'
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers### Warning 19.40,
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sieversignoring declaration for builtin identifier '__<=>__'
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sievers### Hint 22.14,
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sieversno kind found for 's'
7a43e910ce00eef22fd42925ae4c85cbea1b1320Kay Sievers expected: {Cpo}
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers found: {Type}
c55b1b59b837dfd924b704d457ed77c55f8bfeabLennart Poettering### Hint 22.14,
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sieversno kind found for 's'
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers expected: {Cppo}
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sievers found: {Type}
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering### Warning 22.8,
59704f3e937c664f7324bfbb08483c358dfbc4c6Lennart Poetteringignoring declaration for builtin identifier '__=__'
59704f3e937c664f7324bfbb08483c358dfbc4c6Lennart Poettering### Hint 27.8, redeclared type '__->?__'
59704f3e937c664f7324bfbb08483c358dfbc4c6Lennart Poettering### Hint 30.8, redeclared type '__*__'
9ec82de1725ddaab333149171b790d62c47ae133Lennart Poettering*** Error 31.6-31.12, illegal type pattern '__ * __ * __'
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering### Hint 40.7, not a class 's'
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering### Hint 42.16, rebound variable 'x'
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering### Hint 39.14-39.19,
7f8732835295fce29479b1afc9e8ee801852db09Lennart Poetteringrepeated declaration of 'def' with type 'Pred s'
7f8732835295fce29479b1afc9e8ee801852db09Lennart Poettering### Hint 44.15, rebound variable 'x'
7f8732835295fce29479b1afc9e8ee801852db09Lennart Poettering### Hint 39.14-39.19,
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poetteringrepeated declaration of 'tt' with type 'Pred s'
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering*** Error 46.11, unexpected mixfix token: und
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering### Hint 50.8, redeclared type '__->__'
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering### Hint 52.8, redeclared type '__->__'
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering### Hint 52.18, repeated supertype '__->?__'
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering*** Error 54.42-54.49,
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poetteringambiguous mixfix term
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering*** Error 54.6, unexpected mixfix token: :
603cd8fe07cb03e8b11722d1a732e569e5a46347Lennart Poettering### Hint 58.13, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 58.6,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringignoring declaration for builtin identifier '__res__'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 59.9, rebound variable 'x'
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering### Hint 60.14, rebound variable 'x'
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering### Hint 60.14, rebound variable 'x'
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart Poettering### Warning 60.9-60.26,
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poetteringillegal lhs pattern
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poettering'(var snd : s * t ->? t) ((var x : s), (var y : t)) : t'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering*** Error 65.18-65.30,
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poetteringambiguous mixfix term
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers def (x res y)
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers def (x res y)
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers*** Error 65.51-65.69,
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieversambiguous mixfix term
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers### Hint 65.7, rebound variable 'x'
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sievers*** Error 65.18-65.30, unexpected term 'def (x res y)'
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sievers### Hint 65.40, rebound variable 'x'
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering*** Error 65.51-65.69, unexpected term '(def y) und (def x)'
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering### Hint 65.7, rebound variable 'x'
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering*** Error 65.18-65.30, unexpected term 'def (x res y)'
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering### Hint 65.40, rebound variable 'x'
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering*** Error 65.51-65.69, unexpected term '(def y) und (def x)'
1b89884ba31cbe98f159ce2c7d6fac5f6a57698fLennart Poettering*** Error 65.16,
1b89884ba31cbe98f159ce2c7d6fac5f6a57698fLennart Poetteringambiguous typings
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering 1. (\ ((var x : s), (var y : t)) . def (x res y))
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering= \ ((var x : s), (var y : t)) . (def y) und (def x)
15abdb9a6f34628b04b887e0b9649fa582d6cd37Lennart Poettering 2. (\ ((var x : s), (var y : t)) . def (x res y))
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering= \ ((var x : s), (var y : t)) . (def y) und (def x)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 72.11,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringno kind found for 's'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering expected: {Cpo}
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 72.11,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringno kind found for 's'
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering expected: {Cppo}
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering### Hint 74.5, rebound variable 'x'
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering### Hint 74.5, rebound variable 'x'
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering### Hint 75.6, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 75.35, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 75.35, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 75.6, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 75.35, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 75.35, rebound variable 'x'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 85.6, new type shadows type variable 's'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering*** Error 85.11, illegal type variable as supertype 's'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 87.40,
f801968466fed39d50d410b30ac828c26722cc95Lennart Poetteringin type of '(pred eq : forall s : Type . s * s)'
de34a42bcad31f0648ac0f249801310e0dbf83f9Lennart Poettering typename 'Unit' (72.9)
de34a42bcad31f0648ac0f249801310e0dbf83f9Lennart Poettering is not unifiable with type 'Unit ->? Unit' (87.33)
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering### Hint 87.40,
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poetteringuntypeable term (with type: _v371 ->? Pred Unit) 'eq'
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering*** Error 87.38,
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poetteringno typing for 'program all (p : Pred s) : Pred Unit = eq (p, tt)'
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poettering### Hint 90.14, rebound variable 'x'
a1cccad1fe88ddd6943e18af97cf7f466296970fLennart Poettering### Hint 90.45, no type found for 't1'
a1cccad1fe88ddd6943e18af97cf7f466296970fLennart Poettering### Hint 90.45, no type found for 't1'
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering### Hint 90.45,
d05c556b6b2a680ec8b51ecbbc99a9ab14c28eedZbigniew Jędrzejewski-Szmekuntypeable term (with type: ? (_v390 ->? _v389 ->? Unit ->? Pred Unit))
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering### Hint 90.45-90.47,
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poetteringuntypeable term (with type: _v390 ->? _v389 ->? Unit ->? Pred Unit)
4a30847b9d71e0381948d68279c8f775b9de7850Lennart Poettering### Hint 90.45-90.50,
5e8b28838e493b59628322b69580097ef7dd9384Lennart Poetteringuntypeable term (with type: _v389 ->? Unit ->? Pred Unit)
d87be9b0af81a6e07d4fb3028e45c4409100dc26Lennart Poettering### Hint 90.45, no type found for 't1'
d87be9b0af81a6e07d4fb3028e45c4409100dc26Lennart Poettering### Hint 90.45, no type found for 't1'
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering### Hint 90.45,
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringuntypeable term (with type: ? (_v392 ->? _v391 ->? ? Pred Unit))
38a60d7112d33ffd596b23e8df53d75a7c09e71bLennart Poettering### Hint 90.45-90.47,
d8b78264a5245307babbf5af8e39d6d4a1ae095fLennart Poetteringuntypeable term (with type: _v392 ->? _v391 ->? ? Pred Unit)
d8b78264a5245307babbf5af8e39d6d4a1ae095fLennart Poettering### Hint 90.45-90.50,
d8b78264a5245307babbf5af8e39d6d4a1ae095fLennart Poetteringuntypeable term (with type: _v391 ->? ? Pred Unit) 't1 () und'
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poettering### Hint 90.45-90.54,
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poetteringuntypeable term (with type: ? Pred Unit) 't1 () und t2'
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering*** Error 90.43,
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering'program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()'
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering*** Error 93.11, unexpected mixfix token: impl
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering*** Error 95.11, unexpected mixfix token: or
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering### Hint 98.39, no type found for 'all'
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering### Hint 98.39,
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poetteringuntypeable term (with type: _v409 ->? Pred Unit) 'all'
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poettering'program ex (p : Pred s) : Pred Unit
5aea932fd54db835b77709ddeba30732648aae53Lennart Poettering = all \ r : Pred Unit . (all \ x : s . p x impl r) impl r'
5aea932fd54db835b77709ddeba30732648aae53Lennart Poettering### Hint 101.29, no type found for 'all'
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart Poettering### Hint 101.29,
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart Poetteringuntypeable term (with type: _v420 ->? Pred Unit) 'all'
fd4d89b2c0b31da01d134301e30916931ae3c7d9Lennart Poettering### Hint 101.9, rebound variable 'ff'
fd4d89b2c0b31da01d134301e30916931ae3c7d9Lennart Poettering### Hint 101.29, no type found for 'all'
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poettering### Hint 101.29,
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poetteringuntypeable term (with type: _v421 ->? Pred Unit) 'all'
4d9909c93e9c58789c71b34555a1908307c6849eLennart Poettering*** Error 101.27,
47ae7201b1df43bd3da83a19e38483b0e5694c99Lennart Poettering'program ff () : Pred Unit = all \ r : Pred Unit . r ()'
47ae7201b1df43bd3da83a19e38483b0e5694c99Lennart Poettering### Hint 103.42,
88a6c5894c9d3f85d63b87b040c130366b4006ceKay Sieversin type of '(var r : Unit ->? Unit)'
8351ceaea9480d9c2979aa2ff0f4982cfdfef58dLennart Poettering typename 'Unit'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering is not unifiable with type '_v436 ->? Pred Unit' (103.49)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 103.42,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringuntypeable term (with type: _v437 ->? _v436 ->? Pred Unit) 'r'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 103.42-103.44,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringuntypeable term (with type: _v436 ->? Pred Unit) 'r impl'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering*** Error 103.40,
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poetteringno typing for 'program neg (r : Pred Unit) : Pred Unit = r impl ff'
c649f72baed31c54c8384c3ca1d203fab6e98d08David Strauss### Hint 108.3, no type found for 'all'
c649f72baed31c54c8384c3ca1d203fab6e98d08David Strauss### Hint 108.3, untypeable term (with type: _v440 ->? Unit) 'all'
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering*** Error 108.3-108.63,
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering \ (f, g) : s ->? t
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering . all \ x : s . eq (\ . f x, g x) impl eq (f, g)'
3471bedc005fab03f40b99bf6599645330adcd9eLennart Poettering### Warning 115.7, unchanged class 'Cpo'
3471bedc005fab03f40b99bf6599645330adcd9eLennart Poettering### Hint 117.5, is type variable 'c'
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart Poettering### Hint 119.16,
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart Poetteringno kind found for 'c'
59cea26a349cfa8db906b520dac72563dd773ff2Lennart Poettering expected: {Cppo}
9473414219330b9febc1d0712bbf49ad74cf962fLennart Poettering### Hint 121.3, no type found for 'all'
f1a8e221ecacea23883df57951e291a910463948Lennart Poettering### Hint 121.3, untypeable term (with type: _v442 ->? Unit) 'all'
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poettering*** Error 121.3-121.16, no typing for 'all \ x : c . x <<= x'
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poettering### Hint 122.3, no type found for 'all'
5b40d33761376354116a8cddb9b9fbdb6c4727d6Lennart Poettering### Hint 122.3, untypeable term (with type: _v445 ->? Unit) 'all'
5b40d33761376354116a8cddb9b9fbdb6c4727d6Lennart Poettering*** Error 122.3-122.44,
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering'all \ (x, y, z : c) . (x <<= y) und (y <<= z) impl x <<= z'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers### Hint 123.3, no type found for 'all'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers### Hint 123.3, untypeable term (with type: _v448 ->? Unit) 'all'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers*** Error 123.3-123.57,
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sieversno typing for
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers'all \ (x, y, z : c) . (x <<= y) und (y <<= x) impl eq (x, y)'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers### Hint 125.32, no type found for 'all'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers### Hint 125.32, untypeable term (with type: _v451 ->? _v452) 'all'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers*** Error 125.14-125.46,
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sieversno typing for '(all \ n : nat . s n <<= s (Suc n)) as Unit'
d3a3f22267a7dac426b07a7ed0baa1632f5daf04Kay Sievers### Hint 126.15, rebound variable 'x'
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering### Hint 126.38, no type found for 'all'
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering### Hint 126.38, untypeable term (with type: _v455 ->? _v456) 'all'
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering*** Error 126.14-126.52,
e01a15b71e18bf2008aec7e75041ffa42eb80b80Kay Sieversno typing for '(all \ n : nat . s n <<= x) as Unit'
a888b352eb53b07daa24fa859ceeb254336b293dLennart Poettering*** Error 130.21-131.74,
98ef27df896f36f0407eaa7ed9e295203b9c271bLennart Poetteringambiguous mixfix term
a0a3844815b0f346dba03f41245c620f432e462fLennart Poettering def (((sup s) impl)
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers ((((isBound (sup s, s)) und) all)
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x)))
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers ((def (sup s)) impl)
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers((((isBound (sup s, s)) und) all)
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x))
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sievers### Hint 130.3, no type found for 'all'
b8217b7bd5fd171916a095b150fad4c3a37f5a41Kay Sievers### Hint 130.3, untypeable term (with type: _v458 ->? Unit) 'all'
18b754d345ecb0b15e369978aaffa72e9814b86aKay Sievers*** Error 130.3-131.74,
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering \ s : nat -> c
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart Poettering . def (sup s) impl
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart Poettering (isBound (sup s, s) und all
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poettering (\ x : c . isBound (x, s) impl sup (s) <<= x))'
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poettering### Hint 134.3, no type found for 'all'
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poettering### Hint 134.3, untypeable term (with type: _v460 ->? Unit) 'all'
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poettering*** Error 134.3-134.46,
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poetteringno typing for 'all \ s : nat -> c . isChain s impl def (sup s)'
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering### Hint 139.5, is type variable 'p'
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poettering### Warning 141.4,
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poetteringignoring declaration for builtin identifier 'bottom'
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering### Hint 143.3, no type found for 'all'
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering### Hint 143.3, untypeable term (with type: _v462 ->? Unit) 'all'
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering*** Error 143.3-143.22, no typing for 'all \ x : p . bottom <<= x'
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering### Hint 148.6, is type variable 'f'
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart Poettering### Hint 150.15-150.17, is type list '[f]'
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart Poettering### Hint 119.14-119.18,
abd55b16547d0bb0ed1c31e72e16838f0f59f48bKay Sieversrepeated declaration of '__<<=__' with type 'c * c ->? Unit'
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poettering### Hint 153.5, is type variable 'c'
a6e87e90ede66815989ba2db92a07102a69906feLennart Poettering### Hint 153.5, rebound type variable 'c'
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering### Hint 153.8, is type variable 'd'
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering### Hint 155.17, redeclared type '__*__'
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering### Hint 157.7, not a class 'c'
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering### Hint 157.11, not a class 'c'
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering### Hint 157.18, not a class 'd'
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poettering### Hint 157.23, not a class 'd'
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poettering### Hint 159.10, rebound variable 'x1'
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering### Hint 159.14, rebound variable 'y1'
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering### Hint 159.23, rebound variable 'x2'
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart Poettering### Hint 159.27, rebound variable 'y2'
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart Poettering### Hint 159.37,
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversin type of '(pred __<<=__ : forall c : Cpo . c * c)'
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers typename 'Unit' (119.14)
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers is not unifiable with type '_v477 ->? _v476 ->? Unit' (159.53)
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering### Hint 159.37,
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poetteringuntypeable term (with type: _v478 ->? _v477 ->? _v476 ->? Unit)
7d441ddb5ca090b5a97f58ac4b4d97b3e84fa81eLennart Poettering### Hint 159.37,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringuntypeable term (with type: _v477 ->? _v476 ->? Unit) 'x1 <<= x2'
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poettering### Hint 159.33-159.45,
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poetteringuntypeable term (with type: _v476 ->? Unit) '(x1 <<= x2) und'
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering*** Error 159.31,
d3c7d7dd77b2b72315164b672462825cef6c0f9aKay Sieversno typing for
72b9ed828bd22f3ddd74b6853c183eebf006d6d8Lennart Poettering'program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)'
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering### Hint 169.9, redeclared type '__-->?__'
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering### Hint 169.20, repeated supertype '__->?__'
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering*** Error 171.24-171.61,
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringambiguous mixfix term
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering (def (((f x) und) x)) <<= y
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering (((def (f x)) und) x) <<= y
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering*** Error 174.45, unexpected mixfix token: +
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering*** Error 173.28-174.61,
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poetteringambiguous mixfix term
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering def ((((f (s m)) und) eq)
7c697168102cb64c5cb65a542959684014da99c7Lennart Poettering (sup (\ n : nat .! f (s (n + m))), f (sup s)))
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering ((((def f) (s m)) und) eq)
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering(sup (\ n : nat .! f (s (n + m))), f (sup s))
8d0e38a2b966799af884e78a54fd6a2dffa44788Lennart Poettering*** Error 170.7, unexpected mixfix token: :
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering### Hint 176.16-176.25, is type list '[c -->? d]'
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering*** Error 176.41-176.68,
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poetteringambiguous mixfix term
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering (def ((((f x) impl) f) x)) <<= (g x)
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering ((((def (f x)) impl) f) x) <<= (g x)
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering### Warning 176.11, variable also known as type variable 'f'
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering### Hint 176.31, no type found for 'all'
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering### Hint 176.31, untypeable term (with type: _v502 ->? Unit) 'all'
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poettering*** Error 176.29,
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering'program f <<=[c -->? d] g
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering = all \ x : c . def (f x) impl f (x) <<= g (x)'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 179.17, redeclared type '__-->__'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Warning 181.17-181.23, non-unique kind for '__ -->? __'
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering### Hint 181.9, redeclared type '__-->__'
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering### Hint 181.19, repeated supertype '__-->?__'
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering### Hint 182.16,
21bdae12e11ae20460715475d8a0c991f15464acLennart Poetteringno kind found for 'd'
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering expected: {Cppo}
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering*** Error 182.46-182.53,
796b06c21b62d13c9021e2fbd9c58a5c6edb2764Kay Sieversambiguous mixfix term
7a2a0b907b5cc60f5d9a871997d7d6e7f62bf4d8Lennart Poettering*** Error 182.7, unexpected mixfix token: :
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering### Hint 184.7, not a kind 'c --> d'
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart Poettering### Hint 184.19,
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart Poetteringno kind found for 'd'
8bbabc447b1d913bd21faf97c7b17d20d315d2b4Lennart Poettering expected: {Cppo}
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering### Warning 184.6, variable also known as type variable 'f'
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering### Hint 184.11, not a kind 'c --> d'
a73d88fa024b5668ed7dde681e99547d41e6a864Lennart Poettering### Hint 184.19,
a74a8793b04de9886b4f6987b9cb86fa02c73520Lennart Poetteringno kind found for 'd'
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poettering expected: {Cppo}
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poettering### Hint 186.25-186.34, is type list '[c -->? d]'
44143309dd0b37d61d7d842ca58f01a65646ec71Kay Sievers### Hint 186.10, rebound variable 'f'
3d57c6ab801f4437f12948e29589e3d00c3ad9dbLennart Poettering### Warning 186.10, variable also known as type variable 'f'
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering### Hint 186.16, rebound variable 'g'
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sievers### Hint 186.10, rebound variable 'f'
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering### Warning 186.10, variable also known as type variable 'f'
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering### Hint 186.16, rebound variable 'g'
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering### Hint 119.14-119.18,
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poetteringrepeated declaration of '__<<=__' with type 'c * c ->? Unit'
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering### Hint 190.16,