The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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