Stream: Coq users

Topic: Bind notation argument to notation scope


view this post on Zulip Fabian Kunze (Nov 13 2020 at 08:49):

Is it possible to open a scope (using %scopeName) for some argument of a notation? For example, i know that P below always is a list, and would therefore like list_scope to be opened there.

Notation "'≃≃(' P ',' S ')'" := (tspec (P,S)) (at level 0, P at level 200, S at level 200, no associativity, format "'≃≃(' P ','  S ')'").

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:54):

For the argument of a notation, I don't know, but it is certainly possible for the argument of a function, using the Arguments command.

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 08:55):

https://coq.github.io/doc/v8.12/refman/language/extensions/arguments-command.html#binding-to-scope

view this post on Zulip Fabian Kunze (Nov 13 2020 at 08:57):

Yes, and for the record, one can even enable the automatic declaration of these annotations for all new functions with arguments of a certain type using Bind Scope.

view this post on Zulip Fabian Kunze (Nov 13 2020 at 08:58):

The problem in my use case that P is a list and S is a vector and I don't have a good idea on how to get "++" available on both sides.

view this post on Zulip Yannick Forster (Nov 13 2020 at 09:53):

You probably thought of that, but what's the reason writing ( P % list_scope, S % vector_scope)) doesn't work?

view this post on Zulip Fabian Kunze (Nov 13 2020 at 10:03):

I have to test again, but i think it was that % was treated as an part of the notation I define.

view this post on Zulip Paolo Giarrusso (Nov 13 2020 at 12:29):

I think Yannick’s idea is the correct fix, and I’ve used it in the past. “treated as part of the notation” sounds odd, please show us the attempt :-)

view this post on Zulip Paolo Giarrusso (Nov 13 2020 at 12:32):

semi-relevant caveats:

view this post on Zulip Paolo Giarrusso (Nov 13 2020 at 12:33):

view this post on Zulip Fabian Kunze (Nov 13 2020 at 13:15):

Oh, I put the "%" on the LHS, but of course, on the RHS, it works:
Notation "'≃≃(' P ',' S ')'" := (tspec (P%list,S%vector)) (at level 0, P at level 200, S at level 200, no associativity, format "'≃≃(' P ',' S ')'").

The problem for me was related to me forgetting that scopes are not considered during parsing, but only after parsing is done, to figure out how to replace the parsed notations with the right terms.


Last updated: Jan 29 2023 at 01:02 UTC