The Coq mailing list

[t x <txrev319 AT gmail.com>]

Sorry, I wasn't clear -- "creating a list" is not meant to be a hardcoded portion of the notation.

So, for example, I would also want:

MAGIC_START "hello"

( ( BEGIN 1; 2 END) , (BEGIN 2; 3 END) , (BEGIN 3; 4 END) )

END_MAGIC

to end up creating Tuples with the first argument bound to "hello".

So in general, I'm looking for something that lets me "nest" notations so that I can do:

OUTER_DEFINE "some-value"

... doing some wordk here ...

  ... some other notation can refer to "some-value" ...

END_OUTER_DEFINE

On Mon, Sep 2, 2013 at 8:59 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

Hi,

You can use recursive notations (note the ..). For the partial
application, I simply use normal abstraction. Hope it helps!

Notation "'BEGIN' b ; c 'END'" :=
  (fun a=>foos a b c) (at level 60).

Notation "'MAGIC_START' h f1 .. fn 'END'"
  :=  (cons (f1 h) (.. (cons (fn h) nil) ..)).

Eval simpl in MAGIC_START "hello"
  BEGIN 1 ; 2 END
  BEGIN 2 ; 3 END
  BEGIN 3 ; 4 END
END.

On Mon, Sep 2, 2013 at 10:36 AM, t x <txrev319 AT gmail.com> wrote:
> 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!