coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrew Kennedy <akenn AT microsoft.com>
- To: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Notations for patterns
- Date: Fri, 11 Mar 2011 23:23:25 +0000
- Accept-language: en-GB, en-US
It seems to be a bug in Coq 8.2, fixed in Coq 8.3, though not listed as such
in the release notes.
Cheers
Andrew.
-----Original Message-----
From: AUGER Cedric
[mailto:Cedric.Auger AT lri.fr]
Sent: 11 March 2011 10:22
To: Andrew Kennedy
Cc:
coq-club AT inria.fr
Subject: Re: [Coq-Club] Notations for patterns
Le Fri, 11 Mar 2011 07:41:03 +0000,
Andrew Kennedy
<akenn AT microsoft.com>
a écrit :
> Hi all
>
> I'd like to define a notation that doubles up as both a term and a
> pattern. As far as I can tell, Coq has a look at the right-hand-side
> of the Notation definition and attempts to interpret it as both a term
> and a pattern, but unfortunately doesn't tell you when it fails to
> interpret it as a pattern until you actually use it. I'm having
> problems persuading Coq to accept notations for patterns that contain
> "_" standing for *index* arguments. This works:
>
> Inductive BITS :=
> | NIL : BITS
> | CONS : bool -> BITS -> BITS.
>
> Notation "b .0" := (CONS false b) (at level 2).
>
> Definition LSBZero x := match x with b.0 => true | _ => false end.
>
> It even works if I spuriously parameterize BITS:
>
> Inductive BITS (n:nat) :=
> | NIL : BITS n
> | CONS : bool -> BITS n -> BITS n.
>
> Notation "b .0" := (CONS _ false b) (at level 2).
>
> Definition LSBZero (x : BITS 5) := match x with b.0 => true | _ =>
> false end.
>
> But now if I try and *index* BITS by a nat, it fails:
>
> Inductive BITS : nat -> Type :=
> | NIL : BITS 0
> | CONS : forall n, bool -> BITS n -> BITS (S n).
>
> Notation "b .0" := (CONS _ false b) (at level 2).
>
> Definition LSBZero (x:BITS 5) := match x with b.0 => true | _ => false
> end.
>
>
> I get the following error in the definition of LSBZero:
Quite strange, it works on my version of coq.
Are you sure you have no other notations which may enter in conflict with the
one you did?
>
> Toplevel input, characters 97-100:
> Error: Invalid notation for pattern.
>
> Any idea what Coq doesn't like?
> Cheers
> Andrew.
>
>
- [Coq-Club] Notations for patterns, Andrew Kennedy
- Re: [Coq-Club] Notations for patterns,
AUGER Cedric
- RE: [Coq-Club] Notations for patterns, Andrew Kennedy
- Re: [Coq-Club] Notations for patterns,
AUGER Cedric
Archive powered by MhonArc 2.6.16.