Stream: Coq users

Topic: ✔ Making a new notation scope


view this post on Zulip Julin S (Jan 11 2022 at 07:31):

How can we make a new notation scope in coq?

I tried something but that gave error:

Notation "x << y" := (Nat.ltb x y) (at level 1) : new_scope.

Compute (3 << 4)%new_scope.
(*
Unknown scope delimiting key new_scope.
*)

What am I doing wrong?

To create a new scope, isn't mentioning it while the first notation of that scope is being defined enough?

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 07:47):

The name of a scope (new_scope) and its key (%key) are independent. You need to use the Delimit Scope command to associate a key to a scope.

view this post on Zulip Julin S (Jan 11 2022 at 08:29):

Thanks. It worked with:

Notation "x << y" := (Nat.ltb x y) (at level 1) : new_scope.
Declare Scope new_scope.
Delimit Scope new_scope with new.

Compute (3 << 4)%new.

view this post on Zulip Notification Bot (Jan 11 2022 at 08:30):

Julin S has marked this topic as resolved.

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 08:31):

Note that it does not make much sense to use Declare Scope after you have already put a notation in the scope.

view this post on Zulip Julin S (Jan 11 2022 at 08:50):

Oh, because new_scope is implicitly declared when the notation was specified to be in that scope?


Last updated: Jan 29 2023 at 06:02 UTC