Andrej Bauer wrote:
> Jacques Carette said he would be happy with an intensional notion of 
> equality of functions. Surely Jacques, you would want some guarantees 
> about such an equality to make it useful, otherwise one could just define
>
>   let reallySillyIntensionalEquality f g = false

I really meant 'Intensional equality', in other words, if they are the 
same as far as the system is concerned (in a logic this usually this 
means the same syntactically, but in the case of ocaml that would be 
pointer equality).

> So are you suggesting something other than ocaml's == ? What 
> guarantees would you expect?

I was under the impression that ocaml's == did funny things with respect 
to floats?  I want an equality that is "powerful" on ground values and 
== on functional values (ie no exceptions when == is not true).

Jacques