The Coq mailing list

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

Yeah. Simple unfolding of symbolic names in patterns would be nice, though, for the reasons I mentioned. On the other hand, I guess it'd arguably be a hack that breaks design symmetry. Maybe it'd cause other problems, too. Thanks, --k

On Wed, Oct 8, 2014 at 2:07 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Just like in ML and Haskell, those positions don't make sense with arbitrary expressions.  You need patterns there, and it would add nontrivial complexity to the Gallina design to introduce more first-class treatment of patterns.  [Definition] introduces new _expression_ constructs.

On 10/08/2014 02:05 PM, Kevin Sullivan wrote:

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