The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

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