[Ur] MY_ORD = resolving eq class instance / functor?

[Adam Chlipala]

Marc Weber wrote:
>> 2) Extend the definition of [strict_less a] to contain an [eq a], too.
>> (Though this seems to create some dissonance with the words "strict less"!)
>>      
> That would have been
>
> structure My_Ord
>    class strict_less a = (eq a) ->  a ->  a ->  bool
>    ...
> ?
>    

No, it would be a pair of values, like
     eq a * (a -> a -> bool)
or perhaps a record would be nicer.