32a2f5f00ff72c095b39629101043db4407974f9Christian Maederclass Eq < Type

32a2f5f00ff72c095b39629101043db4407974f9Christian Maederclass Ord < Eq

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype a : Ord

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop f : forall e : Ord . e -> e

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop c : a

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder. f (f c) = c;

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype t : Eq

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop b : t

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder. f b = b;

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederEq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedera : Ord

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederb : t %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederc : a %(op)%

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

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

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder unresolved constraints '{t : Ord}'