As far as I know, if the same notation has different meanings in different scopes, then the most-recently-opened scope has priority. For example:
Require Import ZArith Int63. Local Open Scope int63_scope. Local Open Scope Z_scope. Locate "+". (* default interpretation is Z.add *)
Then I would expect that
Check (to_Z (2 << 1 + 1)).
would fail, because
2 << 1 is an
... + 1 would be interpreted in
Z by default. However, Coq accepts this, interpreting the
+ as the
Check (2 << 1 + 1).
does fail with
Error: The term "2 << 1" has type "int" while it is expected to have type "Z".
as I expected. What is going on?
That's because the first argument of
to_Z has the
Nice, I wasn't aware that arguments could have assigned scopes. How would I set that up for a new definition? Is it just an automatic consequence of the argument's type? What if there are several scopes related with that type?
Arguments command allows assigning scopes to arguments manually. As you have guessed, one may associate a type (more precisely, a coercion class) to a scope using the
Bind Scope command, and then it becomes automatic. https://github.com/coq/coq/blob/3915bc904fc16060c25baaf7d5626e3587ad2891/theories/Numbers/Cyclic/Int63/PrimInt63.v#L36
IIUC, at most one scope can be associated with a coercion class. Setting these scopes of arguments automatically is done when one declares a constant (such as
to_Z) or an inductive type.
Thank you, this has been very helpful!
A gotcha: You’ll want to call Bind Scope for a type foo as soon as foo is defined, for things to work well.
If you don’t, when you do call Bind Scope, the scopes of existing functions will be updated retroactively, but the scopes of existing notations will not.
Last updated: Jan 27 2023 at 01:03 UTC