Частичное применение не допускается при использовании функции

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.

EDIT после обратной связи от Маркуса: node_t является конструктор tree который подпись terminal -> tree: данный термин foo типа terminal, node_t foo имеет тип дерева. node имеет подпись non_terminal -> tree_list -> tree.

У вас есть объявленные неявные параметры? В противном случае в ваших случаях match вы применяете слишком много аргументов до node и node_t, что может быть интерпретировано как частичное приложение.