The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Z,

Le 2 mars 10 à 11:46, 
zell08v AT orange.fr
 a écrit :

> Hello everyone,
>
> I have a very naive question:
>
> Do you think  there is a built-in syntactic equality that ensures  
> the usage of
> [rewrite], if you know what I mean by that vague "syntactic  
> equality" ?

The are various notions of equality in Coq, but mainly two of  
interest: definitional
equality (alpha-beta-delta-...- conversion) and propositional  
(Leibniz.eq).
[rewrite] is supposed to be used with propositional equalities, while  
you can use
[change] to transform definitionally equal terms. I'm not sure what  
you mean by
<< ensuring the usage of rewrite >> though.

-- M.