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?
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.
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.
Note that it does not make much sense to use
Declare Scope after you have already put a notation in the scope.
new_scope is implicitly declared when the notation was specified to be in that scope?
Last updated: Jan 29 2023 at 06:02 UTC