ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder. (op f[a] : forall e : Ord . e -> e)

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

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder = (op c : a)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop b : t

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederEq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder? : +Type -> Type

d48085f765fca838c1d972d2123601997174583dChristian MaederLogical : Type := ? Unit

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian MaederUnit : Type

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 Maedera : Ord

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq

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

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

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

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

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

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

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

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederb : t %(op)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederbottom : forall a : Type . a %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederc : a %(op)%

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederfalse : Unit %(fun)%

41859342472c9349707a4bbd7a05340c639013c0Christian Maedernot__ : ? Unit ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertrue : Unit %(fun)%

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Sentences -------------------------------------------------------------

c7041924e85535e80c7c08699cb308071d7010beChristian Maederf (f c) = c

c7041924e85535e80c7c08699cb308071d7010beChristian Maederf b = b

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

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 16.3, constrain 't : Ord' is unprovable

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder known kinds are: Eq

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

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder unresolved constraints '{ t : Ord }'