Skip to Content.

Sympa Menu

coq-club - [Coq-Club] more coq black magic : variable -> string

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] more coq black magic : variable -> string

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] more coq black magic : variable -> string
Date: Mon, 2 Sep 2013 09:06:40 +0000

Hi,

Suppose I have the following:

Definition a := 10.
Definition b := 20.

Is it possible to define

Notation "'MAGIC' x 'END'" := ...

such that

MAGIC (a) = ("a", 10).

and

MAGIC (b) = ("b", 20).

I can promise that 'x' is an ident. I'm just looking for something that will go from symbol -> string representing variable name.

Thanks!

[Coq-Club] more coq black magic : variable -> string, t x, 09/02/2013

Archive powered by MHonArc 2.6.18.