The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

You can solve the readability problem by using abbreviations instead of definitions.

Notation foo  := 1.

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

http://coq.inria.fr/coq/refman/Reference-Manual014.html#Abbreviations

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Oct 8, 2014 at 2:05 PM, Kevin Sullivan <sullivan.kevinj AT gmail.com> 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