ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder. (fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)(op c : a)),

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder op c : a)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq

9df7943e174665a367e75714d54b352a3760dd58Christian Maederop b : t

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder. (fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Classes ---------------------------------------------------------------

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederEq < Type

d48085f765fca838c1d972d2123601997174583dChristian MaederOrd < Eq

d48085f765fca838c1d972d2123601997174583dChristian Maeder%% Type Constructors -----------------------------------------------------

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian MaederLogical : Type := Unit ->? Unit

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian MaederUnit : Type := Unit

117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__*__ : Type+ -> Type+ -> Type

117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__-->__ : Type- -> Type+ -> Type

117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder__-->?__ : Type- -> Type+ -> Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : Type- -> Type+ -> Type

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

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maedera : Ord

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maedert : Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Assumptions -----------------------------------------------------------

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

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

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

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

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder__when__else__

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederb : t %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederbottom : forall a : Type . a_v-1 %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederc : a %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederf : forall e : Ord . e_v-1 -> e_v-1 %(op)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederfalse : Unit %(fun)%

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

41859342472c9349707a4bbd7a05340c639013c0Christian Maedertrue : Unit %(fun)%

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

41859342472c9349707a4bbd7a05340c639013c0Christian Maeder%% Sentences -------------------------------------------------------------

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder(fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

c7041924e85535e80c7c08699cb308071d7010beChristian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)

c7041924e85535e80c7c08699cb308071d7010beChristian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)(op c : a)),

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder op c : a)

d48085f765fca838c1d972d2123601997174583dChristian Maeder(fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

117f087bc4e24ad34fac1bf8aa4385681bba4524Christian Maeder ((op f[t] : forall e : Ord . e_v-1 -> e_v-1)(op b : t), op b : t)

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder%% Diagnostics -----------------------------------------------------------

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder*** Error 16.7, unresolved constraint 't : Ord'

*** Hint 16.7,

expected: Ord

found: Eq