The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/05/2016 11:05 AM, Hugo Herbelin wrote:
> Hi Jonathan,
>
> As an extra note: Applications are parsed at level 10 and arguments of
> applications at level 9. Such as the LL-style camlp4/5 underlying
> parsing engine works, putting "| x |" at level < 10, i.e. at the level
> of potential arguments of an application, would make that for
> expressions of the form "| ident |" or "| ... + ident |", etc., the
> parser would try to interpret "ident" applied to some argument
> starting with "|" rather than seeing the "|" as matching the currently
> opened "|".
>
> Best,
>
> Hugo

I guess that's what the following fragment from "Print Grammar constr" 
means:

| "10" LEFTA
  [ SELF; LIST1 constr:appl_arg

I can deal with "| x |" at level 10, although this means having to 
parenthesize it for function arguments - but maybe I will compensate by 
turning most such functions into operators (at higher levels) themselves.

Thanks,
Jonathan

> On Wed, May 04, 2016 at 05:17:24PM -0400, Jonathan Leivent wrote:
> > On 05/04/2016 04:56 PM, James Lottes wrote:
> > > I've been using
> > > Notation "| x |" := (abs x) (at level 50, format "| x |").
> > > Though it's not without problems. It works well enough for me in most
> > > parsing contexts (certainly not all), but tends to display with extra
> > > parentheses: (|x|). For example, this works for me:
> > >
> > > Lemma abs_triangle : |x+y| ≤ |x|+|y|.
> > >
> > > I'll also be keen to hear if there's a better way.
> > >
> > > Cheers,
> > > James
> > Interesting.  Apparently, it works for levels >= 10, but not for
> > levels < 10.   OK - I will try 10.
> >
> > Thanks,
> > -- Jonathan
> >
> > > On Wed, May 4, 2016 at 10:38 AM, Jonathan Leivent 
> > > <jonikelee AT gmail.com>
> > >  wrote:
> > > > I would like to have:
> > > >
> > > >    Notation "| x |" := (length x) (at level 0) : nat_scope.
> > > >
> > > > However, it seems that using vertical bars this way causes problems for the
> > > > parser (Syntax error: [constr:operconstr level 200] expected after '|' (in
> > > > [constr:operconstr])).  Putting the notation at level 200 means I'd have to
> > > > parenthesize it for virtually all uses.  I thought by restricting this
> > > > notation to nat_scope, I would get around the parser problems, but I can't
> > > > get this to work.
> > > >
> > > > Is this just not possible?  If it is possible, what is the proper
> > > > incantation?
> > > >
> > > > This is in 8.5pl1.
> > > >
> > > > -- Jonathan