The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Sorry, I had problems with my mail client and thought it did not sent my previous atempts.

2013/5/28 AUGER Cedric <sedrikov AT gmail.com>

Le Tue, 28 May 2013 14:05:01 -0700,
Math Prover <mathprover AT gmail.com> a écrit :

> Thanks! I previously failed to see ":=" meant Definition. :-)
>
>
> On Tue, May 28, 2013 at 1:23 PM, Pierre-Marie Pédrot <
> pierre-marie.pedrot AT inria.fr> wrote:
>
> > On 28/05/2013 22:20, Math Prover wrote:
> >
> >> How do I do "rewriting" with terms of the form "a := ... " instead
> >> of "H: _ = _"
> >>
> >
> > "unfold a in ..." instead of "rewrite a in ..."
> >
> > PMP
> >

There is also the subst tactic which works for both equality and
definition.

--
.../Sedrikov\...