Constrain.hascasl.output revision d48085f765fca838c1d972d2123601997174583d
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederop f : forall e : Ord . e -> e
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. ((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) :
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Classes ---------------------------------------------------------------
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Type Constructors -----------------------------------------------------
d48085f765fca838c1d972d2123601997174583dChristian Maeder? : +Type -> Type
d48085f765fca838c1d972d2123601997174583dChristian MaederLogical : Type := ? Unit
117f087bc4e24ad34fac1bf8aa4385681bba4524Christian MaederPred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__*__ : +Type -> +Type -> Type
117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type
117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : -Type -> +Type -> Type < __->?__
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->?__ : -Type -> +Type -> Type
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)%
47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maederbottom : forall a : Type . a_v-1 %(fun)%
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((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) :
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Diagnostics -----------------------------------------------------------
d48085f765fca838c1d972d2123601997174583dChristian Maeder*** Hint 16.3, constrain 't : Ord' is unprovable
117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder known kinds are: [ Eq ]
d48085f765fca838c1d972d2123601997174583dChristian Maeder*** Error 16.3, 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 Unit' of type 'Unit'
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder unresolved constraints '{ t : Ord }'