我正在尝试使用 Coq 中的列表删除函数 standard library但它要求输入奇怪的内容，我不知道如何解决。
我正在实现的功能是在 lambda 项中创建一个自由变量列表，如下所示:
Fixpoint fv (t : trm) : vars :=
match t with
| Var v => [v]
| App t1 t2 => (fv t1) ++ (fv t2)
| Abs x t' => remove x (fv t')
end.
它给了我以下错误:
Error: In environment
fv : trm -> vars
t : trm
x : nat
t' : trm
The term "x" has type "nat" while it is expected to have type
"forall x0 y : ?171, {x0 = y} + {x0 <> y}".
我很确定删除函数的定义中与假设有关。我不知道如何处理它，有什么帮助吗？
最佳答案
remove 在包含以下内容的上下文中定义:
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
函数removes将此作为第一个参数(您可以通过执行Printremove看到。)
这个假设是一个函数，决定列表中类型元素的相等性。在你的情况下，你必须提供一个函数来决定 var 的相等性(这似乎是 nat，所以标准库中也可能有这样的函数) .
如果您不知道“{p} + {q}”表示法，可以在这里查找: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool
关于coq - 使用列表删除功能，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/20998889/