coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to handle " := " in hypothesis?

From: Math Prover <mathprover AT gmail.com>
To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to handle " := " in hypothesis?
Date: Tue, 28 May 2013 14:05:01 -0700

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

[Coq-Club] How to handle " := " in hypothesis?, Math Prover, 05/28/2013
- Re: [Coq-Club] How to handle " := " in hypothesis?, Pierre-Marie Pédrot, 05/28/2013
  - Re: [Coq-Club] How to handle " := " in hypothesis?, Math Prover, 05/28/2013
    - Message not available
      - Re: [Coq-Club] How to handle " := " in hypothesis?, Cedric Auger, 05/28/2013