coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] matching a part of name

From: Erkki Luuk <erkkil AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] matching a part of name
Date: Mon, 16 Oct 2017 23:16:32 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=erkkil AT gmail.com; spf=Pass smtp.mailfrom=erkkil AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f169.google.com
Ironport-phdr: 9a23:Vxoh/hTtS9YwDPm09e3eqG+OU9psv+yvbD5Q0YIujvd0So/mwa67YRSN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YAFyP6H+HpPYp8WxzeG7vZPJMCtSgz/oTKlxLxT+iRjMtYFCjJFhKac14hTMq3pMPe9RwDU7dhqogx/g65Lor9ZY+CNKtqd5+g==

Hi all

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)

Best

Erkki

[Coq-Club] matching a part of name, Erkki Luuk, 10/16/2017
- Re: [Coq-Club] matching a part of name, Hugo Herbelin, 10/17/2017
  - Re: [Coq-Club] matching a part of name, Erkki Luuk, 10/19/2017