如何解决Coq 中的列表构造函数冲突
我在 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
上的长返回在另一个地方工作正常。这是一个类似记忆的模拟。
关于为什么会发生这种情况的任何想法?
解决方法
符号 ::
脱糖为 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。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。