使用记录中的符号

Question

Coq手册(术语和符号的同时定义(规定

由于保留了符号、归纳、共归纳、记录，递归和共草书定义可以使用自定义符号。

我想定义一些类似的东西

Reserved Notation "A +' B" (at level 80).
Record foo T :=
{ add : T -> T ->T;
commute a b : a +' b = b +' a 
where "a +' b" := (add a b)
}.

但我有

Error: Unknown interpretation for notation "_ +' _".

Answer 1

在Record中首次使用之前必须定义符号，如下所示：

Reserved Notation "A +' B" (at level 60).
Record foo T :=
{ add : T -> T ->T where "A +' B" := (add A B);
commute a b : a +' b = b +' a 
}.