coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations
Chronological Thread
- From: t x <txrev319 AT gmail.com>
- To: Beta Ziliani <beta AT mpi-sws.org>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations
- Date: Mon, 2 Sep 2013 09:02:25 +0000
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: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!
- [Coq-Club] "context aware / lexical scoping / partial application" Notations, t x, 09/02/2013
- Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations, Beta Ziliani, 09/02/2013
- Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations, t x, 09/02/2013
- Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations, Beta Ziliani, 09/02/2013
- Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations, t x, 09/02/2013
- Re: [Coq-Club] "context aware / lexical scoping / partial application" Notations, Beta Ziliani, 09/02/2013
Archive powered by MHonArc 2.6.18.