Coq表示法语法错误：[term level 200]之后应为[term level 200] (在[term]中)

Question

我对Coq/Gallina中的Notation感到困惑。我已经把我的问题变成了一个最小的例子:为什么在下面的最后一行不能工作？

Definition nOp (a b:nat) := a.
Notation "'nOpOpen' a b 'nOpClose'" := (nOp a b).
Definition foo0 := (nOp 1 0).
Definition foo1 := (nOpOpen 1 0 nOpClose).
//this last line gives
//Syntax error: [term level 200] expected after [term level 200] (in [term]).

Answer 1

以这种方式设置级别对我来说很有效：

Notation "'nOpOpen' a b 'nOpClose'" := (nOp a b) 
  (at level 10, a at next level, b at next level).