FunctorMonadTransformer.hascasl.output revision b99471d6e14282504e4ec6e13a64568097ee8619
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederclass Functor < Type -> Type
e83ed59502a681713982f25c559aae77a4145734Christian Maeder {vars f : Functor; a, b, c : Type
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder op map : (a -> b) -> f a -> f b
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski vars x : f a; f : a -> b; g : b -> c
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . (map \ y : a .! y) x = x
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder . (map \ y : a .! g (f y)) x = map g (map f x);
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederclass Monad < Type -> Type
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder {vars m : Monad; a, b, c : Type
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ops __>>=__ : m a * (a ->? m b) ->? m b;
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder __>>=__ : m a * (a -> m b) -> m b;
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski ret : a -> m a
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder vars x, y : a; p : m a; q : a ->? m b; r : b ->? m c; f : a ->? b
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . def q x => ret x >>= q = q x
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . (p >>= \ x : a . ret (f x) >>= r) = p >>= \ x : a . r (f x)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . p >>= ret = p
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . (p >>= q) >>= r = p >>= \ x : a . q x >>= r
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . (ret x : m a) = ret y => x = y;
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederclass instance Monad < Functor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervars m : Monad; a, b : Type; f : a -> b; x : m a
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder. map f x = x >>= \ y : a . ret (f y);
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederclass MonadT < Monad -> Monad
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder {vars t : MonadT; m : Monad; a : Type
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder op lift : m a -> t m a
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder vars x : a; p : m a; b : Type; q : a -> m b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . lift (ret x) = (ret x : t m a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . lift (p >>= q) = lift p >>= \ y : a .! lift (q y) : t m b;
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervar state : Type
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype instance ST state : Monad
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervars a, b : Type
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype ST state a := state ->? a * state
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervars x : a; p : ST state a; q : a ->? ST state b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder%% Classes ---------------------------------------------------------------
e83ed59502a681713982f25c559aae77a4145734Christian MaederFunctor < Type -> Type
e83ed59502a681713982f25c559aae77a4145734Christian MaederMonad < Functor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederMonadT < Monad -> Monad
e83ed59502a681713982f25c559aae77a4145734Christian Maeder%% Type Constructors -----------------------------------------------------
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederST : Type -> Monad := \ state : Type . _t1030
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder_t1030 : Type -> Type := \ a : Type . state ->? a * state
e83ed59502a681713982f25c559aae77a4145734Christian Maeder%% Type Variables --------------------------------------------------------
e83ed59502a681713982f25c559aae77a4145734Christian Maedera : Type %(var_1026)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederb : Type %(var_1027)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederc : Type %(var_85)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederf : Functor %(var_1)%
e83ed59502a681713982f25c559aae77a4145734Christian Maederm : Monad %(var_752)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederstate : Type %(var_1024)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedert : MonadT %(var_751)%
e83ed59502a681713982f25c559aae77a4145734Christian Maeder%% Assumptions -----------------------------------------------------------
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder__>>=__ : forall m : Monad; a : Type; b : Type
e83ed59502a681713982f25c559aae77a4145734Christian Maeder . m a * (a -> m b) -> m b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder__>>=__ : forall m : Monad; a : Type; b : Type
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . m a * (a ->? m b) ->? m b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederlift : forall t : MonadT; m : Monad; a : Type . m a -> t m a %(op)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedermap : forall f : Functor; a : Type; b : Type
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . (a -> b) -> f a -> f b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederret : forall m : Monad; a : Type . a -> m a %(op)%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder%% Variables -------------------------------------------------------------
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederp : ST state a
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederq : a ->? ST state b
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder%% Sentences -------------------------------------------------------------
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder(map \ y : a .! y) x = x
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder(map \ y : a .! g (f y)) x = map g (map f x)
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederdef q x => (__>>=__ : m a * (a ->? m b) ->? m b) (ret x, q) = q x
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder(__>>=__ : m a * (a ->? m c) ->? m c)
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder(p, \ x . (__>>=__ : m b * (b ->? m c) ->? m c) (ret (f x), r))
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder= (__>>=__ : m a * (a ->? m c) ->? m c) (p, \ x . r (f x))
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder(__>>=__ : m a * (a ->? m a) ->? m a) (p, ret) = p
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder(__>>=__ : m b * (b ->? m c) ->? m c)
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian Maeder((__>>=__ : m a * (a ->? m b) ->? m b) (p, q), r)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski= (__>>=__ : m a * (a ->? m c) ->? m c)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (p, \ x . (__>>=__ : m b * (b ->? m c) ->? m c) (q x, r))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder(ret x : m a) = ret y => x = y
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder= (__>>=__ : m a * (a ->? m b) ->? m b) (x, \ y . ret (f y))
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maederlift (ret x) = (ret x : t m a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederlift ((__>>=__ : m a * (a ->? m b) ->? m b) (p, q))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder= (__>>=__ : t m a * (a ->? t m b) ->? t m b)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (lift p, \ y .! lift (q y) : t m b)
e83ed59502a681713982f25c559aae77a4145734Christian Maeder%% Diagnostics -----------------------------------------------------------
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 2.7, is type variable 'f'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 2.19, is type variable 'a'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 2.22, is type variable 'b'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 2.25, is type variable 'c'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 4.8, not a kind 'f a'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 4.16, not a class 'a'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 4.16, not a class 'b'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 4.27, not a class 'b'
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder### Hint 4.27, not a class 'c'
58564afba8f0bb6b57783c4b440d0b666edf5f67Christian Maeder### Hint 9.7, is type variable 'm'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 9.17, is type variable 'a'
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder### Hint 9.17, rebound type variable 'a'
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder### Hint 9.20, is type variable 'b'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 9.20, rebound type variable 'b'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 9.23, is type variable 'c'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 9.23, rebound type variable 'c'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 13.8, not a class 'a'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 13.7, rebound variable 'x'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 13.11, not a class 'a'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 13.17, not a kind 'm a'
f624c6980131e5b0598e00e7d8b4acb9720f8996Christian Maeder### Hint 13.25, not a kind 'a ->? m b'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 13.39, not a kind 'b ->? m c'
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder### Hint 13.53, not a kind 'a ->? b'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 13.52, rebound variable 'f'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 14.14-14.24, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a) (var x : a),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (var q : a ->? m b))'
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski### Hint 14.14-14.24, untypable term (with type: _v106_m _v107_a * (_v107_a -> _v106_m _v108_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 15.12, rebound variable 'x'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 15.19-15.33, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder ((var f : a ->? b) (var x : a)),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (var r : b ->? m c))'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 15.19-15.33, untypable term (with type: _v203_m _v204_a * (_v204_a -> _v203_m _v205_b))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder '(ret (f x), r)'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 15.3-15.33, rejected '__->?__ < __->__' of '((var p : m a),
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder \ (var x : a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . (op __>>=__ :
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ((op ret : forall m : Monad; a : Type . a -> m a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ((var f : a ->? b) (var x : a)),
e83ed59502a681713982f25c559aae77a4145734Christian Maeder (var r : b ->? m c)))'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 15.3-15.26, untypable term (with type: _v166_m _v167_a * (_v167_a -> _v166_m _v168_b))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder '(p, \ x : a . ret (f x) >>= r)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 15.12, rebound variable 'x'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 15.19-15.33, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ((var f : a ->? b) (var x : a)),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (var r : b ->? m c))'
dc427a9450cd7b463717a2255c804afa47a54365Christian Maeder### Hint 15.19-15.33, untypable term (with type: _v254_m _v255_a * (_v255_a -> _v254_m _v256_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder '(ret (f x), r)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 16.13, rebound variable 'x'
dc427a9450cd7b463717a2255c804afa47a54365Christian Maeder### Hint 16.5-16.25, rejected '__->?__ < __->__' of '((var p : m a),
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \ (var x : a)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . (var r : b ->? m c) ((var f : a ->? b) (var x : a)))'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 16.5-16.25, untypable term (with type: _v304_m _v305_a * (_v305_a -> _v304_m _v306_b))
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder '(p, \ x : a . r (f x))'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 16.13, rebound variable 'x'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.4-18.10, rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 18.4-18.10, untypable term (with type: _v446_m _v447_a * (_v447_a -> _v446_m _v448_b))
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder### Hint 18.3-18.17, rejected '__->?__ < __->__' of '((op __>>=__ :
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ((var p : m a), (var q : a ->? m b)),
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (var r : b ->? m c))'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 18.3-18.17, untypable term (with type: _v410_m _v411_a * (_v411_a -> _v410_m _v412_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder '(p >>= q, r)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.4-18.10, rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 18.4-18.10, untypable term (with type: _v482_m _v483_a * (_v483_a -> _v482_m _v484_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.29, rebound variable 'x'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.36-18.44, rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder### Hint 18.36-18.44, untypable term (with type: _v555_m _v556_a * (_v556_a -> _v555_m _v557_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.21-18.44, rejected '__->?__ < __->__' of '((var p : m a),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder \ (var x : a)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . (op __>>=__ :
e83ed59502a681713982f25c559aae77a4145734Christian Maeder forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)
e83ed59502a681713982f25c559aae77a4145734Christian Maeder ((var q : a ->? m b) (var x : a), (var r : b ->? m c)))'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 18.21-18.36, untypable term (with type: _v518_m _v519_a * (_v519_a -> _v518_m _v520_b))
e83ed59502a681713982f25c559aae77a4145734Christian Maeder '(p, \ x : a . q x >>= r)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.29, rebound variable 'x'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 18.36-18.44, rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 18.36-18.44, untypable term (with type: _v600_m _v601_a * (_v601_a -> _v600_m _v602_b))
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 20.16, refined class 'Monad'
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder### Hint 21.7, is type variable 'm'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 21.7, rebound type variable 'm'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 21.17, is type variable 'a'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 21.17, rebound type variable 'a'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 21.20, is type variable 'b'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 21.20, rebound type variable 'b'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 21.30, not a class 'a'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 21.30, not a class 'b'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 21.29, rebound variable 'f'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 21.41, not a kind 'm a'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 21.40, rebound variable 'x'
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder### Hint 22.21, rebound variable 'y'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 22.13-22.35, rejected '__->?__ < __->__' of '((var x : m a),
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \ (var y : a)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder . (op ret : forall m : Monad; a : Type . a -> m a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ((var f : a -> b) (var y : a)))'
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski### Hint 22.13-22.35, untypable term (with type: _v699_m _v700_a * (_v700_a -> _v699_m _v701_b))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder '(x, \ y : a . ret (f y))'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 22.21, rebound variable 'y'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 25.7, is type variable 't'
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder### Hint 25.18, is type variable 'm'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 25.18, rebound type variable 'm'
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder### Hint 25.28, is type variable 'a'
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder### Hint 25.28, rebound type variable 'a'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 27.8, not a class 'a'
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder### Hint 27.7, rebound variable 'x'
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder### Hint 27.14, not a kind 'm a'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 27.13, rebound variable 'p'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 27.21, is type variable 'b'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 27.21, rebound type variable 'b'
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski### Hint 27.31, not a kind 'a -> m b'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 27.30, rebound variable 'q'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 29.33, rebound variable 'y'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder### Hint 29.33, rebound variable 'y'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 29.33, rebound variable 'y'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 29.33, rebound variable 'y'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 31.7, is type variable 'state'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 33.7, is type variable 'a'
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder### Hint 33.7, rebound type variable 'a'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 33.10, is type variable 'b'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 33.10, rebound type variable 'b'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 34.6, redeclared type 'ST'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 35.8, not a class 'a'
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder### Hint 35.7, rebound variable 'x'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 35.14, not a kind 'ST state a'
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder### Hint 35.13, rebound variable 'p'
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder### Hint 35.29, not a kind 'a ->? ST state b'
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder### Hint 35.28, rebound variable 'q'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder### Hint 36.7, in type of '(var x : a)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder typename 'a' (35.10)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder is not unifiable with type 'a * state' (36.20)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 36.7, untypable term (with type: a * state)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder### Hint 36.3-36.42, untypable term (with type: ? _v1033_a * ? _v1033_a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder '(ret x : ST state a, \ s : state . (x, s))'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder*** Error 36.3, no typing for '(ret x : ST state a) = \ s : state . (x, s)'
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder### Hint 37.3-37.9, in type of '((var p : ST state a), (var q : a ->? ST state b))'
e83ed59502a681713982f25c559aae77a4145734Christian Maeder typename 'a' (35.31)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder is not unifiable with type 'a * state' (35.25)
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski### Hint 37.3-37.9, untypable term (with type: _v1058_m _v1059_a * (_v1059_a -> _v1058_m _v1060_b))
90bf4bf40789422552e566b73738ba5efae144c3Christian Maeder### Hint 37.3-37.9, in type of '((var p : ST state a), (var q : a ->? ST state b))'
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder typename 'a' (35.31)
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski is not unifiable with type 'a * state' (35.25)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 37.3-37.9, untypable term (with type: _v1061_m _v1062_a * (_v1062_a ->? _v1061_m _v1063_b))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 37.5-37.54, untypable term (with type: ? _v1051_a * ? _v1051_a)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder '(p >>= q, \ s1 : state . let (z, s2) = p s1 in q z s2)'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder*** Error 37.5, no typing for 'p >>= q = \ s1 : state . let (z, s2) = p s1 in q z s2'