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 -----------------------------------------------------------

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_9_v9' (10.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type '_var_15_v15 ->? _var_16_v16' (10.6)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_15_v15 ->? _var_16_v16' (10.6)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.6, untypable application (with result type: Unit ->? _var_6_v6)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder 'f(c)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_20_v20' (10.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type '_var_26_v26 ->? _var_27_v27' (10.6)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.8, in type of '(op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 'a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_26_v26 ->? _var_27_v27' (10.6)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 10.6, untypable application (with result type: Unit ->? _var_17_v17)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder 'f(c)'

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder*** Hint 10.3, 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) :

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_17_v17) :

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_18_v18,

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder op c : a)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder type 'a * a' (8.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_4_v4 * _var_5_v5'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 16.5, in type of '(op b : t)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 't' (14.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_32_v32' (16.5)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder*** Hint 16.5, in type of '(op b : t)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder typename 't' (14.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_35_v35' (16.5)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder*** Hint 16.3, 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) :

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder _var_36_v36,

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder op b : t)'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder type 't * t' (14.8)

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder is not unifiable with type 'Unit ->? _var_30_v30 * _var_31_v31'

c6456fd6e9cc28e09be25058d38fd41cc49a87e9Christian Maeder

93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder*** Hint 16.7,

93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder expected: Ord

93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder found: Eq

93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder

cf1821d1617c189cc24428cfa654d3975f73755fChristian Maeder*** Error 16.7, 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 }'