Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Partial application is not allowed while using Function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Partial application is not allowed while using Function


Chronological Thread 
  • From: DAVID PEREIRA <DMRPE AT isep.ipp.pt>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Partial application is not allowed while using Function
  • Date: Sat, 6 Jun 2015 11:58:06 +0000
  • Accept-language: en-US
  • Authentication-results: inria.fr; dkim=none (message not signed) header.d=none;

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.



Archive powered by MHonArc 2.6.18.

Top of Page