The Coq mailing list

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

Hi Pierre,

Thanks a lot for your reply and the link. I have already received a suggestion of using Program Fixpoint instead of Function, so I´ll work on it and come back in case I have further questions.

Best Regards,

Marcus.

2015-06-08 12:38 GMT+01:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

Hi,

Indeed partial application for recursive calls are not supported by Function (see paragraph "Limitations" of https://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#Function). 

Can you give a self contained script please, so that we may suggest a workaround?

Best regards,

Pierre

2015-06-06 11:59 GMT+02:00 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.​