Constrain.hascasl.output revision b645cf3dc1e449038ed291bbd11fcc6e02b2fc7f
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederop f : forall e : Ord . e -> e
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder. ((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a * a ->? Unit)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[a] : forall e : Ord . e_v-1 -> e_v-1) : a -> a)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[a] : forall e : Ord . e_v-1 -> e_v-1) : a -> a)(op c : a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a,
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder op c : a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder Unit
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop b : t
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder. ((fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t * t ->? Unit)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[t] : forall e : Ord . e_v-1 -> e_v-1) : t -> t)(op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t,
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder Unit
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Classes ---------------------------------------------------------------
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederEq < Type
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Type Constructors -----------------------------------------------------
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederLogical : Type := Unit ->? Unit
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian MaederUnit : Type
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__*__ : Type+ -> Type+ -> Type
b789ce4c50283bff24d92a2806b253850395d990Christian Maeder__-->__ : Type- -> Type+ -> Type < (__-->?__, __->__)
b789ce4c50283bff24d92a2806b253850395d990Christian Maeder__-->?__ : Type- -> Type+ -> Type < __->?__
b789ce4c50283bff24d92a2806b253850395d990Christian Maeder__->__ : Type- -> Type+ -> Type < __->?__
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__->?__ : Type- -> Type+ -> Type
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedera : Ord
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Assumptions -----------------------------------------------------------
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__when__else__
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederb : t %(op)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maederbottom : forall a : Type . a_v-1 %(fun)%
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederc : a %(op)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederf : forall e : Ord . e_v-1 -> e_v-1 %(op)%
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederfalse : Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maedernot__ : ? Unit ->? Unit %(fun)%
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertrue : Unit %(fun)%
41859342472c9349707a4bbd7a05340c639013c0Christian Maeder�__ : ? Unit ->? Unit %(fun)%
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Sentences -------------------------------------------------------------
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a * a ->? Unit)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[a] : forall e : Ord . e_v-1 -> e_v-1) : a -> a)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[a] : forall e : Ord . e_v-1 -> e_v-1) : a -> a)(op c : a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder a,
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder op c : a) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder Unit
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder((fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t * t ->? Unit)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[t] : forall e : Ord . e_v-1 -> e_v-1) : t -> t)(op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t,
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder Unit
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Diagnostics -----------------------------------------------------------
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_10_v10'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder is not unifiable with type '_var_13_v13 ->? _var_14_v14' (10.8)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_13_v13 ->? _var_14_v14'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, untypable application (with result type: Unit ->? _var_8_v8)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder 'f(c)'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_21_v21'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder is not unifiable with type '_var_24_v24 ->? _var_25_v25' (10.8)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op c : a)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_24_v24 ->? _var_25_v25'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, untypable application (with result type: Unit ->? _var_19_v19)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder 'f(c)'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint 10.3-10.13, in type of '(((op f[_var_19_v19] : forall e : Ord . e_v-1 -> e_v-1) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_19_v19 -> _var_19_v19)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[_var_21_v21] : forall e : Ord . e_v-1 -> e_v-1) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_21_v21 -> _var_21_v21)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (op c : a) :
8eb681fd73f8eb576072b56c8226cfc76a44ad3cChristian Maeder _var_21_v21) :
8eb681fd73f8eb576072b56c8226cfc76a44ad3cChristian Maeder _var_19_v19,
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder op c : a)'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder type 'a * a' (10.13)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder is not unifiable with type 'Unit ->? _var_3_v3 * _var_3_v3' (10.13)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op b : t)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 't' (14.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_34_v34'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint, in type of '(op b : t)'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 't' (14.8)
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder is not unifiable with type 'Unit ->? _var_37_v37'
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint 16.9, in type of '(((op f[_var_37_v37] : forall e : Ord . e_v-1 -> e_v-1) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_37_v37 -> _var_37_v37)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (op b : t) :
8eb681fd73f8eb576072b56c8226cfc76a44ad3cChristian Maeder _var_37_v37,
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder op b : t)'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder type 't * t' (16.9)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder is not unifiable with type 'Unit ->? _var_29_v29 * _var_29_v29' (16.9)
c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Hint 16.9,
93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder expected: Ord
93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder found: Eq
93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder*** Error 16.9, in term'((fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t * t ->? Unit)
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder (((op f[t] : forall e : Ord . e_v-1 -> e_v-1) : t -> t)(op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder t,
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder op b : t) :
cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder Unit' of type 'Unit'
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder unresolved constraints '{ t : Ord }'