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 `Set`

.

I couldn't find anything on searching online (possibly due to % being a special character or something).

What does % mean in this context?

Here `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.

Thanks!

No it's not a type-cast. If you do

```
Definition foo := 1%nat.
Definition bar := foo%positive.
```

Then `bar`

will still be a natural number and not be cast to `positive`

.

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 `positive`

.

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

```
expression%nat
```

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: Jun 24 2024 at 14:01 UTC