Julin S (Jan 11 2022 at 07:31): 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?
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.
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.
Julin S has marked this topic as resolved.
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.
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: Sep 28 2023 at 11:01 UTC