coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Some questions about tactics in Coq

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Some questions about tactics in Coq
Date: Mon, 12 Sep 2016 09:12:27 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:c7qyExyuip98RO3XCy+O+j09IxM/srCxBDY+r6Qd0uIWIJqq85mqBkHD//Il1AaPBtSCrawUwLSP++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHdvZiN3y3OSv8bXSZR9JjXyze+BcNhKz+C7VN8wbh5dVEqctj17ipnJVd+lSjTdjIV+WkhDgoN+x4LZs9i1Rv7Qq8MsWAvayRLgxUbENVGduCGsy/sC+7RQ=

On 2016-09-12 08:00, Sebastian Böhne wrote:
> 2) When I want to unfold a notation I can first locate it ('locate
> "operator-sign"') and then do an unfold with the real non-abbreviated
> name. However, I would appreciate a direct way. Is there a tactic to
> do so?

Would this work?

Goal 1 + 1 = 2.
unfold "+"
unfold "_ + _". (* also works *)

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Some questions about tactics in Coq, Sebastian Böhne, 09/12/2016
- Re: [Coq-Club] Some questions about tactics in Coq, Gaetan Gilbert, 09/12/2016
- Re: [Coq-Club] Some questions about tactics in Coq, Clément Pit--Claudel, 09/12/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Some questions about tactics in Coq, Sebastian Böhne, 09/18/2016
  - Re: [Coq-Club] Some questions about tactics in Coq, Gaetan Gilbert, 09/18/2016