The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  The answer to this is most likely "it's not possible" but I thought I'd check anyway.

  Here is my min failure case.

Require Import List String ZArith.
Import ListNotations.
Local Open Scope list_scope.


Inductive Foo :=
| foo (s: string) (n1: Z) (n2: Z).


Notation "'BEGIN' a ; b ; c 'END'" :=
(foo a b c).

Eval simpl in BEGIN "hello" ; 1 ; 2 END.

Eval simpl in
     (BEGIN "hello" ; 1 ; 2 END) ::
     (BEGIN "hello" ; 2 ; 3 END) ::
     (BEGIN "hello" ; 3 ; 4 END) :: nil.

(* can I do something like this:

MAGIC_START "hello"
  (BEGIN' 1 ; 2 END') ::
  (BEGIN' 2 ; 3 END') ::
  (BEGIN' 3 ; 4 END') :: nil
MAGIC_END.
and have it generate the same as above ? *)

What I want is to be able to "bind" one of the varaibles i.e. ahve the MAGIC_START somehow remember "hello", then the BEGIN' somehow know to look up the varaible that MAGIC_START has remembered.

Is there some black magic to make this happpen?

Thanks!