The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think this is currently impossible because terms are interpreted before notations are parsed, even if they are not typechecked.  (This is the reason, for example, that we don't have recursive notations; you don't get to defer desugaring and interpretation.)  It's possible that you could jury-rig something in trunk/8.5 using tactics-in-terms and type-classes for pattern matching on supported types (you'd have to add each type as a separate instance, and deep pattern matching would probably be a gigantic pain), where your "p" gets interpreted as some kind of list of open_constrs, and then type-class resolution figures out how to put them back together in the right way, and ... somehow allows them to be treated as binders in "e"?  I wouldn't be surprised if it could be made to work in the appropriate cases, but I wouldn't be surprised if it couldn't either.

It certainly seems worth a feature request on the bug tracker; I don't think I've heard anyone ask for it before.

-Jason

On Fri, Feb 7, 2014 at 12:00 PM, Andrew Kennedy <akenn AT microsoft.com> wrote:

Hello all

 

I often find myself wanting to define notation that abstracts over match *patterns*, not just variables. I am assuming that this is not possible using the current mechanism; are there any plans to add it in future? A good example is the ssreflect extended if syntax (e.g. “if x is y::ys then ys else nil”) that is currently hardwired into ssreflect rather than defined using notation. A common idiom that I would like to define using notation is

trymatch x with p => e

 

which would expand to

match x with p => Some e | _ => None end

In other words, I want to write

Notation “’trymatch’ x ‘with’ p ‘=>’ e” := (match x with p => Some e | _ => None end) (p pattern)

or something similar.

 

-          Andrew.