> Here's another problem: I wrote about 20,000 lines where I used the built in
> equality for
> a particular type (that represented terms in a theorem prover).  Now I want
> to implement
> my own equality function on the type, and never user built-in equality.  I
[...]
> Don
[...]
> email: dsyme@microsoft.com
> ------------------------------------------------------------------------

A quick hack that may helps could be to use the compiler to detect
those applications by redefining the (=) predicate with a type that is
not compatible with the type term. For instance, you may redefine (=)
for integers only (or strings only), and this way you may statically
find applications of generic equality to your term values since they
become ill-typed. Admittedly, this is not perfect, but can be of some
help in a very symbolic code as a theorem prover, where application of
= to values that are not of type term may be sparse.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/