The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Ah, I see. I don't think this is possible, unfortunately.

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