The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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

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
> >>
> >>