b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuclass Eq

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuclass Ord < Eq

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescutype a : Ord

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuop f : forall e : Ord . e -> e

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuop c : a

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu. f (f c) = c;

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescutype t : Eq

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuop b : t

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu. f b = b;

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu%% Classes ---------------------------------------------------------------

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuEq < Type

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuOrd < Eq

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski%% Type Constructors -----------------------------------------------------

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskia : Ord

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskit : Eq

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski%% Assumptions -----------------------------------------------------------

da955132262baab309a50fdffe228c9efe68251dCui Jianb : t %(op)%

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskic : a %(op)%

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskif : forall e : Ord . e -> e %(op)%

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski%% Sentences -------------------------------------------------------------

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskif (f c) = c

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskif b = b

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski%% Diagnostics -----------------------------------------------------------

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski### Hint 16.3, constrain 't : Ord' is unprovable

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski known kinds are: Eq

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

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski unresolved constraints '{t : Ord}'

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski