The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Is there any fast "eq" predicate in Gallina?

By fast, I mean that it tests references only - returning true iff the
two arguments refer to the same reference.  Hence it is analogous to
the Lisp "eq" predicate, whereas the standard equality in Gallina is
analogous to Lisp "equal".  

One would also need the associated lemmas, such as 
eq x y = true -> x = y.

Also, one would need to know about when two references might be eq.
For instance, it is possible to create a highly wasteful functional
language without any reference sharing (such that eq would be false in
all non-reflexive cases), but hopefully Gallina is not that, and that
the ways in which Gallina is not that can be described in a useful way.