Coq Error: Illegal application (Non-functional construction)

Question

coq 的新手，我正在尝试为我的算术表达式语法制作一个小于或等于的符号。编辑：我为表达式添加了我的数据类型。

我的表达式数据类型：

Inductive Exp :=
| num : nat -> Exp
| var : string -> Exp
| add : Exp -> Exp -> Exp
| sub : Exp -> Exp -> Exp
| div : Exp-> Exp -> Exp.

我的条件数据类型：

Inductive Cond :=
| base : bool -> Cond
| bnot : Cond -> Cond
| beq  : Exp -> Exp -> Cond 
| less : Exp -> Exp -> Cond
| band : Cond -> Cond -> Cond.

如您所见，我没有小于或等于的构造函数，这正是我们的老师为练习设计的方式。因此，在对小于或等于进行标记时，我必须使用其他构造函数。这是我的：

Notation "A <=' B" := (bnot (band (bnot (beq A B) bnot(less A B)))) (at level 10).

现在，当我尝试检查以下表达式的类型时：

Check "x" <=' "y".

我收到以下错误：

Illegal application (Non-functional construction): 
The expression "! "x" =' "y"" of type 
"Cond"
cannot be applied to the term
 "bnot" : "Cond -> Cond"

感谢任何帮助，谢谢。

Answer 1

您的符号中缺少括号。

(* no  *) Notation "A <=' B" := (bnot (band (bnot (beq A B) bnot(less A B)))) (at level 10).

(* yes *) Notation "A <=' B" := (bnot (band (bnot (beq A B)) (bnot(less A B)))) (at level 10).