Coq中的列表构造函数冲突

Question

我在Coq中有以下定义：

Inductive list_variable : Type :=
| nil
| cons (s : string) (l : list_variable).

Fixpoint getElement (l : list_variable) (s : Variabile) (v : Address) {struct l} : Address :=
match l with
| nil => v
| str :: nil => (updateValues v ((updateState (updateState s "memPointer" (s("memPointer")+1)) str (s("memPointer"))) "memPointer") undef)
| str :: l => getElement l s v
end.

由于某些原因，最后一行和第二行返回Found a constructor of inductive type list while a constructor of list_variable is expected.

作为参考，str::nil的长期回报在另一个地方可以很好地工作。这是为了一个类似记忆的模拟。

你知道为什么会发生这种情况吗？

Answer 1

符号::被设计成List.cons，而你想要的是构造函数MyModule.cons。如果你想使用::，你必须为它定义一个新的符号：

Inductive list_variable : Type :=
| nil
| cons : ...
.

(* Redefine "::" for new list type *)
Infix "::" := cons.

如果您打算对list和list_variable使用相同的符号，则有必要管理符号作用域。请参阅the Coq manual, the section on notations。