Fabian Kunze (Nov 13 2020 at 08:49): 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 ')'").
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.
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
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.
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.
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?
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.
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 :-)
Paolo Giarrusso (Nov 13 2020 at 12:32):semi-relevant caveats:
Bind Scope foo with type T doesn’t really work with polymorphic functions — like pair above. Scope resolution is done before typechecking, so Bind Scope has the effect of a sequence of Arguments commands Paolo Giarrusso (Nov 13 2020 at 12:33):Bind Scope affects even existing functions (as the manual says), but it doesn’t affect existing notations using those functions. Hence, best use it right after defining a type. 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: Sep 23 2023 at 07:01 UTC