coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] A question about notation.
Date: Mon, 12 Sep 2016 17:13:55 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f176.google.com
Ironport-phdr: 9a23:GwrzGBJJBUaZEsF89dmcpTZWNBhigK39O0sv0rFitYgUIv7xwZ3uMQTl6Ol3ixeRBMOAuqsC1bqd7PyoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMW1HHiPfsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+/xLEVE6E4mYWemQQiBtBRQbfplmuVZDo9yD+q+BV2S+APMSwQ6piChq46KI+aRvtIz0cfxU46nzTi9c42KNfpRu7vFp0wpTJZICOHPV7d6LZO9gdQDwSDY5qSyVdD9bkPMM0BO0bMLMAog==

Hello,

I made a notation and tested it. It was parsed correctly, but it wasn't display.

Where is my mistake?

Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))): set_scope.
Open Scope set_scope.
Check ({1, 2}).

The "check" command displays

fun a : nat => a = 1 \/ a = 2
: nat -> Prop

while I would like to see something like this:

{1, 2}: nat -> Prop

Thank you!

[Coq-Club] A question about notation., Ilmārs Cīrulis, 09/12/2016
- Re: [Coq-Club] A question about notation., Hugo Herbelin, 09/12/2016
  - Re: [Coq-Club] A question about notation., Ilmārs Cīrulis, 09/13/2016