coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: scott constable <sdconsta AT syr.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Definitions for Parsing Compatibility
- Date: Sat, 20 Feb 2016 10:22:46 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
- Ironport-phdr: 9a23:f2SO2hBd7skKJFQZkeMAUyQJP3N1i/DPJgcQr6AfoPdwSP74osbcNUDSrc9gkEXOFd2CrakU1KyL6eu+CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb3osMOCKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs2AXVXkK2hFPBRPZ5Rv+U9+lqSfxsexmxCCyJtzsC704RGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==
Thanks Pierre, this makes sense to me now.
~Scott
On Sat, Feb 20, 2016 at 5:04 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
The original split is not an ltac definition. It is recognized by parsing rule but it does not have a corresponding ltac entry. Therefore if you define a notation with split it will not combine with it, it will hide the original one.Pierre
Le jeudi 18 février 2016, scott constable <sdconsta AT syr.edu> a écrit :Thanks for the responses. I think I understand the problem somewhat, but let me try to make it more concrete. Suppose that I want to define two kinds of split, "split~" for chaining auto after split, and "split*" for chaining tauto after split. So I might do this:Tactic Notation "split" "~" :=split; auto.Tactic Notation "split" "*" :=split; tauto.But Coq rejects the second notation with the error: "Syntax error: '~' or 'with' expected after 'split' (in [tactic:simple_tactic])." Yet when I instead useTactic Notation "split" :=split.Tactic Notation "split" "~" :=split; auto.Tactic Notation "split" "*" :=split; tauto.I no longer get the error. Could someone please explain in the context of this example what went wrong in the first case, and how the second case resolved the issue?Thanks again,~ScottOn Thu, Feb 18, 2016 at 5:17 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:On 17/02/2016 22:51, scott constable wrote:
> What exactly is the purpose of reintroducing existing tactics as
> identical notations?
AFAIK, that's purely a parsing issue.
Since Coq 8.5, some tactics defined in ML are registered as true Ltac as
they do not require parsing rules. Typically, tactics whose grammar is
of the form
"ident" constr₁ ... constrₙ
for any n. Alas, this clashes with some other notations that are indeed
changing the parsing rules. For instance, in the list you mentionned,
"constructor" has a variant "constructor" integer(i). This leads to
various issues that prevent parsing "constructor" alone.
PMP
- [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/17/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre Courtieu, 02/18/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre-Marie Pédrot, 02/18/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/18/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre Courtieu, 02/20/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/20/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre Courtieu, 02/20/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/18/2016
Archive powered by MHonArc 2.6.18.