ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedertype a : Ord

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian 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)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedertype t : Eq

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian 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 -----------------------------------------------------

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}'