The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

I don't know too much about notations, but perhaps this is not completely useless:

It appears that com doesn't have a constructor to represent calling or referencing another com such as subtract_slowly_body.  And presumably that would need its own notation.

You can reproduce the problem with the following simpler example:

Definition foo : com :=

  [[subtract_slowly_body]].

I suppose defining a notation like "'call' x" might be a way to get around parsing limitations.

--Jim

On Tue, Sep 24, 2019 at 4:05 AM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

Any suggestions from the community on how to make custom entries work better here would be greatly appreciated.  We would like to use the new features in the next release of Software Foundations (for which the timeline is rather tight), but right now we are blocked on several things that appear to be either inconveniently rigid in the design or not working as documented.  :-(

Thanks!

    - Benjamin

> On Sep 22, 2019, at 1:33 PM, Konstantinos Kallas <kallas AT seas.upenn.edu> wrote:
>
> Hi all,
>
> We are trying to define the syntax of a simple imperative language using the Custom entries feature but we are encountering some problems. Some of the problems might not be related to custom entries per se, but might be caused by some misuse of the notation feature (due to my lack of understanding of parsing in Coq).
>
> I have attached a file that contains the definitions, some examples that work as expected, and some examples where the parser gets confused (that are annotated with "Question:" comments).
>
> It would be great if someone could give us some hints about what could be the problem or how should we go about solving it.
>
> Thanks,
> Konstantinos