The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

To avoid parsing issue, such as in "g | f | x | y |" whether as "g(|f|, x, |y|)" or as "g(|f(|x|, y)|)", I tend to prefer to use opening characters and closing characters.
┤x├ for instance, retains the overall "|" form, but adds the indication whether we are in an opening or a closing.
Plus there is less risks to intefere with already existing notations, such as "{ x | P }" (for sig, if I remember correctly).

2016-05-05 17:23 GMT+02:00 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