Hi. I came across something like
Require Import Coq.PArith.BinPos. Check 1%positive.
and couldn't figure out what "%" meant here. At first I thought it would be a modulus operation. But
Check positive. said
positive is a
I couldn't find anything on searching online (possibly due to % being a special character or something).
What does % mean in this context?
positive is the name of a notation scope, and the
% opens that scope locally. Some documentation here Opening a notation scope locally.
The use of digits to represent numbers is something you can do in different ways, and Coq lets you customize it. Notation scopes then let you choose which interpretation you want to use.
Here, this just means "Interpret
1 as a term in the type
positive", which as you found is a
Set. The scope name and type name are often chosen to coincide, or at least be suggestive.
Okay. So it's like asking coq to consider
1 as a
positive. Something like type casts in programming languages like C.
No it's not a type-cast. If you do
Definition foo := 1%nat. Definition bar := foo%positive.
bar will still be a natural number and not be cast to
As Jasper was saying, numerals like
1 are only notations, and depending on the context they might have different interpretations. If you just write
1 it will give a different result depending on which scope is open. Using
1%positive, you tell Coq that the most important scope here is
So the notation will be interpreted based on the present environment?
Yes. Notations live in scope, and you can open them inside a module or section with
Open Scope nat_scope.
or locally inside a term with
you could add parentheses to make it clear which part is to be interpreted in which scope:
(0 + 1)%nat
Thanks! Got a better idea now.
Ju-sh has marked this topic as resolved.
Last updated: Jan 29 2023 at 01:02 UTC