coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to handle " := " in hypothesis?
- Date: Tue, 28 May 2013 22:23:11 +0200
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
- Message not available
- Re: [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
Archive powered by MHonArc 2.6.18.