The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Hi all, today I found a situation where I had to use a "match … as _
in … return …" instead of a "match … as <some name used in the returned
type> in … return …" or a "match … in … return …".

I used to believe that "as _" was the default when not needing to bind
the pattern matched expression to the result type.
Is this a new behavior or something I never noticed?
(To be honest, it is not that often that I wish the pattern matched
expression not to be bound to the return type, so the current behavior
does not annoy me much. Still, I am curious of the answer.)

I use a rather old version of Coq (a trunk version from October 2012),
so things may have changed since.

(************************************************)
Fixpoint ord (n : nat) : Type :=
  match n with
  | O => Empty_set
  | S n => option (ord n)
  end.

Inductive T (n : nat) : Type :=
  | Var : ord n -> T n
  | Fun : T (S n) -> T n
  | App : T n -> T n -> T n
  .

Inductive redex (n : nat) : T n -> Type :=
  | ARedex (u : T (S n)) : redex (S n) u -> redex n (Fun n u)
  | LRedex (u v : T n) : redex n u -> redex n (App n u v)
  | RRedex (u v : T n) : redex n v -> redex n (App n u v)
  | BRedex (u : T (S n)) (v : T n) : redex n (App n (Fun n u) v)
  .

Inductive VarRedex (n : nat) (o : ord n) : redex n (Var n o) -> Type := .

Definition vredex n o r : VarRedex n o r :=
  match r as _ (*Woo, first time I have to put an underscore here*)
  in redex _ t return match t with Var _ => VarRedex n o r | _ => unit end
  with ARedex _ _ | LRedex _ _ _ | RRedex _ _ _ | BRedex _ _ => tt end.