coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] is |x| a viable notation?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] is |x| a viable notation?
Date: Wed, 4 May 2016 13:38:10 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f49.google.com
Ironport-phdr: 9a23:Wf0coxeW1Cf6r732nKopg0A4lGMj4u6mDksu8pMizoh2WeGdxc69YB7h7PlgxGXEQZ/co6odzbGG4ua4AydZuMrJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuLOU4R3Wb1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3zaBtQQPogSFPEzM47mzRloQkjqVdoRGsoxFy64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==

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

[Coq-Club] is |x| a viable notation?, Jonathan Leivent, 05/04/2016
- Re: [Coq-Club] is |x| a viable notation?, James Lottes, 05/04/2016
  - Re: [Coq-Club] is |x| a viable notation?, Jonathan Leivent, 05/04/2016
    - Re: [Coq-Club] is |x| a viable notation?, Hugo Herbelin, 05/05/2016
      - Re: [Coq-Club] is |x| a viable notation?, Jonathan Leivent, 05/05/2016
        
        Re: [Coq-Club] is |x| a viable notation?, Cedric Auger, 05/06/2016