The Coq mailing list

[James Lottes <jlottes AT gmail.com>]

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


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