Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] is |x| a viable notation?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: James Lottes <jlottes AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] is |x| a viable notation?
  • Date: Wed, 4 May 2016 13:56:27 -0700
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jlottes AT gmail.com; spf=Pass smtp.mailfrom=jlottes AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f176.google.com
  • Ironport-phdr: 9a23:+diIRRG4bVUi3gJOsSO3U51GYnF86YWxBRYc798ds5kLTJ75pMmwAkXT6L1XgUPTWs2DsrQf27uQ6/qrADFfqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0o8eYOlgXzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0cflxdTSyzC8A33Rd+lsC/9qvZwwwGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=

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



Archive powered by MHonArc 2.6.18.

Top of Page