The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

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.