749074bf849727439f584139415f6a985a8aa875Christian Maederclass Eq

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;

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederclasses

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederEq : Type;

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederOrd : Type

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederclass

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertypes

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedera : Ord;

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop b : t %(op)%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop c : a %(op)%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop f : forall e : Ord . e -> e %(op)%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. f (f c) = c

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. f b = b

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

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder known kinds are: {Eq}

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder unresolved constraints '{t : Ord}'