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 int
and ... + 1
would be interpreted in Z
by default. However, Coq accepts this, interpreting the +
as the int63
one.
But!
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 int63_scope
. See About to_Z.
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?
The 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: Oct 13 2024 at 01:02 UTC