Stream: Coq users

Topic: ✔ [Newbie] What does % do in coq?


view this post on Zulip Julin S (Apr 22 2021 at 01:55):

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?

view this post on Zulip Jasper Hugunin (Apr 22 2021 at 03:01):

Here positive is the name of a notation scope, and the % opens that scope locally. Some documentation here Opening a notation scope locally.

view this post on Zulip Jasper Hugunin (Apr 22 2021 at 03:02):

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.

view this post on Zulip Jasper Hugunin (Apr 22 2021 at 03:04):

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.

view this post on Zulip Julin S (Apr 22 2021 at 03:09):

Okay. So it's like asking coq to consider 1 as a positive. Something like type casts in programming languages like C.
Thanks!

view this post on Zulip Théo Winterhalter (Apr 22 2021 at 06:17):

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.

view this post on Zulip Julin S (Apr 24 2021 at 09:02):

So the notation will be interpreted based on the present environment?

view this post on Zulip Théo Winterhalter (Apr 24 2021 at 09:04):

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

view this post on Zulip Julin S (Apr 24 2021 at 09:05):

Thanks! Got a better idea now.

view this post on Zulip Notification Bot (Jul 16 2021 at 07:36):

Ju-sh has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC