The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Here is a very cut down example that checks in version 8.4pl3:

===============
Inductive Ty := NAT | A.

Inductive Exp : Ty -> Type :=
| CONST: nat -> Exp NAT
| IFZ  : forall t, Exp NAT -> Exp t -> Exp t -> Exp t.

Definition step (t:Ty) (M:Exp t) : Exp t :=
  match M in Exp s return Exp s with
    | CONST c => CONST c
    | IFZ t0 e1 e2 e3 =>
      match e1 with
        | CONST 0 => e2
        | _ => e3
      end
  end.
=================

I want to replace the first match case of [step]  with

     | CONST c => M

so I tried

========================
Program Definition step (t:Ty) (M:Exp t) : Exp t :=
  match M in Exp s return Exp s with
    | CONST c => M
    | IFZ t0 e1 e2 e3 =>
      match e1 with
        | CONST 0 => e2
        | _ => e3
      end
  end.
========================

which fails with:

Error: The variable anonymous' was not found in the current environment.

Thanks for any help with making my Definition work.

--Randy