ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederop f : forall e : Ord . e -> e

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder. (op f[a] : forall e : Ord . e -> e)

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder ((op f[a] : forall e : Ord . e -> e) (op c : a))

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder = (op c : a)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop b : t

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder. (op f[t] : forall e : Ord . e -> e) (op b : t) = (op b : t)

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder%% Classes ---------------------------------------------------------------

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian MaederEq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Type Constructors -----------------------------------------------------

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder? : +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederLogical : Type := ? Unit

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian MaederUnit : Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__*__ : +Type -> +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__->?__ : -Type -> +Type -> Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedera : Ord

41859342472c9349707a4bbd7a05340c639013c0Christian Maedert : Eq

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder%% Assumptions -----------------------------------------------------------

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maederb : t %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederbottom : forall a : Type . a %(fun)%

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maederc : a %(op)%

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederf : forall e : Ord . e -> e %(op)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maederfalse : Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedernot__ : ? Unit ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maedertrue : Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder�__ : ? Unit ->? Unit %(fun)%

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder%% Sentences -------------------------------------------------------------

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederf (f c) = c

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederf b = b

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Diagnostics -----------------------------------------------------------

47a19e4d083d2cecf1fd95f93dcbe04496544a6aChristian Maeder*** Hint 16.3, constrain 't : Ord' is unprovable

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder known kinds are: [ Eq ]

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder*** Error 16.3, in term '(op f[t] : forall e : Ord . e -> e) (op b : t) = (op b : t)' of type 'Unit'

93bf2fdad447e4bb6332ea3d3a0eb9cf293e7550Christian Maeder unresolved constraints '{ t : Ord }'

93ee71ae78c3b7419930a8e4a06977ac7dbae6d0Christian Maeder