我想要我自己的范围，来玩弄长的分布。
Declare Scope my_scope.
Delimit Scope my_scope with my.
Open Scope my_scope.
Definition f (x y a b : nat) : nat := x+y+a+b.
Notation "x < y * a = b" := (f x y a b)
(at level 100, no associativity) : my_scope.
Check (1 < 2 * 3 = 4)%my.
你如何制作一个新的范围？
编辑：我选择“x < y * a = b”来覆盖 Coq 的运算符（每个运算符都有不同的优先级）。
该命令Declare Scope不存在。Coq 手册的第 12.2 节描述了有关范围的各种命令。
您对示例符号的选择存在固有问题，因为它与预定义的符号冲突，这些符号似乎在您的符号之前使用。
在查看第一个组件时，解析器看到_ < _ 并认为您实际上是在谈论整数的比较，然后它将第二部分视为符号的实例_ * _，然后它看到所有这一切都是等式的左侧。解析器一直很高兴，它构造了一个形式的表达式：
(1 < (2 * 3)) = 4
这是由解析器构造的，尚未请求类型系统。类型检查器将自然数视为第一个孩子(_ < _)并且很高兴。它认为(_ * _)是第二个孩子，它很高兴，它现在知道该产品的第一个孩子应该是一个 nat 数字，它仍然很高兴；最后它有一个等式，这个等式的第一个组成部分在 type 中Prop，但第二个组成部分在 type 中nat。
如果您键入Locate "_ < _ * _ = _".答案，则会告诉您您确实定义了一个新符号。问题是这个符号永远不会被使用，因为解析器总是找到另一个它以前可以使用的符号。理解为什么一个符号比另一个符号更受欢迎需要更多的解析技术知识，正如 Coq 手册第 12 章的句子中提到的那样（对我来说晦涩难懂）：
Coq 可扩展解析由本质上是 LL1 解析器的 Camlp5 执行。
您必须选择各种变量的水平，x, y, a, 等，b这样这些变量中的任何一个都不能匹配太多的文本。例如，我尝试定义一个接近你的符号，但有一个开始和一个结束括号（我想这大大简化了任务）。
Notation "<< x < y * a = b >>" := (f x y a b)
(x at level 59, y at level 39, a at level 59) : my_scope.
的水平x选择低于 的=水平， y 的水平选择低于 的水平*， 的水平a选择低于的水平=。通过阅读命令的答案获得级别Print Grammar constr. 它似乎工作，因为以下命令被接受。
Check << 1 < 2 * 3 = 4 >>.
但是您可能需要包含更多的工程才能获得真正好的符号。
要回答标题中的实际问题：
当您声明使用它的符号时，就会创建新范围。也就是说，您不会my_scope单独声明新范围。你只写
Notation "x <<< y" := (f x y) (at level 100, no associativity) : my_scope.
并声明了一个新的范围my_scope。
这个问题的答案只适用于旧版本的 Coq。我不确定它是什么时候开始的，但至少在 Coq 8.13.2 中，Coq 更喜欢用户首先使用Declare Scope创建一个新范围。OP 在他们的代码中拥有的是 Coq 现在声明范围的首选方式。
参见当前手册