The Coq mailing list

[Erkki Luuk <erkkil AT gmail.com>]

Ok, thanks. BTW, here's where I got the idea that it might be possible: https://github.com/coq/coq/pull/100#commitcomment-13158222

​Erkki​

​

On Tue, Oct 17, 2017 at 1:43 PM, Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

> I want to match a part of a name, something like in this minimal example:
>
> Inductive foo := f_h | g_h | bar.
> Definition f (x:foo) := match x with
> | _"_h"   => Set
> | _ => Prop end. (* Error: Such pattern cannot have arguments. *)
>
> Is there a way to do this? The code should work w/out modifications if I add
> more names like this (for my purposes it doesn't matter if the fixed part is
> prefixed or suffixed)

What you'd like is not supported. It could in theory be provided but
it is unclear that it is worth the implementation (and relative
complications) knowing that an alternative is to organize the
constructors differently, capturing all the _h variants at the same
time as e.g. in:

Inductive foo_h := f_h | g_h.
Inductive foo := foo_hs (x:foo_h) | bar.
Definition f (x:foo) := match x with
| foo_hs _ => Set
| _ => Prop end.

You can then add new constructors to the auxiliary type foo_h and have
the definition of your function f unchanged.

Best,

Hugo Herbelin