The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Yes. I just want some syntactic support to make this lighter weight. (Maybe 
it can be done with clever notation now?). Bonus points if your solution 
supports nested patterns. 

The classic example is wanting to match a string based on regexps.

-Greg

> On Oct 8, 2014, at 3:46 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
> 
>> On 10/08/2014 03:14 PM, Greg Morrisett wrote:
>> This is an instance of a more general problem with datatypes/inductive
>> definitions that arises in the ML/Haskell/Coq/etc. community:  pattern
>> matching does not promote abstraction.
>> 
>> I’ve always wanted to have more control over this in the form of
>> an abstract pattern declaration (with attendant proofs that the
>> patterns are exhaustive and non-overlapping.)
>> 
>> -Greg
> 
> Aren't you just requesting the common "dependent view" idiom? Define a new 
> inductive type with constructors that are the patterns you want, then 
> define a total function mapping the original type(s) to the view type.  
> Think of the classic isEven/isOdd example.
> 
> -- Jonathan