The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

​Dear Members,

I get this error message for the following piece of Coq script, but I have no idea what is wrong. Can anyone give me some advice? 

"failure in proveterminate

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

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.

Besides the Reference Manual, does anybody know of an alternative source of information on Function, if possible with comments and examples?

Thanks in advance,

Marcus.​