coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
- [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
- Re: [Coq-Club] is |x| a viable notation?, Jonathan Leivent, 05/05/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/04/2016
- Re: [Coq-Club] is |x| a viable notation?, James Lottes, 05/04/2016
Archive powered by MHonArc 2.6.18.