The Coq mailing list

[DAVID PEREIRA <DMRPE AT isep.ipp.pt>]

Olá Marcus,

Acabei de ver a tua mensagem! Se quiseres eu posso tentar ajudar-te… consegues dar-me mais algum context (por exemplo o ficheiro em que ela falha)? Se quiseres manda-me o ficheiro e eu tento ajudar-te aqui…

Um alternativa pode ser usares of Program Fixpoint (embora este seja melhor para raciocinar sobre funções com tipos dependentes).

Diz coisas ;-)

Um abraço,

David

From: Marcus Ramos
Reply-To: <coq-club AT inria.fr>
Date: Saturday 6 June 2015 10:59
To: "coq-club AT inria.fr"
Subject: [Coq-Club] Partial application is not allowed while using Function

​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.​