4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederclass Eq

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederclass Ord < Eq

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedertype a : Ord

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiop f : forall e : Ord . e -> e

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederop c : a

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder. f (f c) = c;

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedertype t : Eq

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederop b : t

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder. f b = b;

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederclasses

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederEq < Type;

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederOrd < Eq

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertypes

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maedera : Ord;

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedert : Eq

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maederop b : t %(op)%

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maederop c : a %(op)%

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

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder. f (f c) = c

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder. f b = b

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

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder known kinds are: {Eq}

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

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder unresolved constraints '{t : Ord}'

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder