The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/03/2014 11:22 AM, Cédric wrote:
> ...
> I guess Coq will never warn against unused variables:
> that would not mix very well with the interactive features.
> "refine (match x with A => _ | B => _ end)." will never raise a 
> warning as '_' is to be filled later.
>
> I would prefer to disallow variables as patterns, but that would break 
> compatibility with already existing developements, and many people 
> won’t be happy if this feature were to be removed (I am not one of 
> them as I never need nor use it, and because as far as I can remember, 
> there is no support internally for this, and the matching is expanded, 
> well I may be wrong on this last point and/or things can have changed).

Would it be difficult to add a slight sugaring of match - call it 
matchlet - that is expanded to match internally, but which does a check 
at (or just after) parsing time for variable vs. constant usage?  The 
matchlet syntax would either require the explicit declaration of the 
variables at the head of the matchlet or in each branch.  So, for example:

  matchlet ... in
  | [X] Foo X Y => ...

would require that X is a variable and Y is not.  For readability 
purposes, it would also be nice if there was a way to make Coq print 
matches as matchlets.

I am pretty sure I've seen something like this in some language, but I 
don't remember where.

-- Jonathan