The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

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:

Toplevel input, characters 97-100:
Error: Invalid notation for pattern.

Any idea what Coq doesn't like?
Cheers
Andrew.