The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I'm wondering what's the technical reason that Coq doesn't unfold expressions in pattern position?

(* THIS WORKS *)

Definition bar (n:nat): nat := match n with 1 => 1 | _ => 0 end.

(* THIS DOESN'T *)

Definition foo: nat := 1.

Definition bar (n:nat): nat := match n with foo => 1 | _ => 0 end.

(* 

The only difference is the use of a symbol rather than a "manifest constant" in the second case.

When using nats to represent objects of another kind, I'd prefer to match on symbolic names rather than on their concrete representations as nats -- for  abstraction, information hiding, readability. Of course the question generalizes beyond nats.

*)

Kevin