使用函数时不允许部分应用

Question

我得到以下错误消息：

"failure in proveterminate Error: Partial application of function convert_btree_to_tree in its body is not allowed while using Function"

从下面的Coq脚本中，我不知道哪里出了问题。有人能给我一些建议吗？

Function convert_btree_to_tree (t: btree (non_terminal' non_terminal terminal) terminal) {measure (fun t => bheight _ _ t)}: 
tree (non_terminal' non_terminal terminal) terminal:=
let tl:= decompose t in
let ttl:= map convert_btree_to_tree tl in
let ttl':= convert_list_tree_to_tree_list ttl in
match broot _ _ t with
| inl n => node _ _ n ttl'
| inr t => node_t _ _ t
end.

关于函数的文档在参考手册中非常有限，如果可能的话，有没有人知道更完整和详细的参考资料，以及注释和示例？

Answer 1

我不太了解Function，但是在你的match中，你会返回一个node和一个node_t。由于您没有给出定义，我不知道这两个构造函数是否来自同一类型，但我认为您有一个拼写错误，第二种情况应该返回node t _ _ t。

根据Marcus的反馈进行编辑：node_t是签名为terminal -> tree的tree的构造函数:给定terminal类型的术语foo，node_t foo的类型为树。node的签名是non_terminal -> tree_list -> tree。

您是否声明了任何隐式参数？否则，在您的match案例中，您会向node和node_t应用太多参数，这可能会被解释为部分应用程序。