coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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.
- [Coq-Club] Partial application is not allowed while using Function, Marcus Ramos, 06/06/2015
- Re: [Coq-Club] Partial application is not allowed while using Function, DAVID PEREIRA, 06/06/2015
- Re: [Coq-Club] Partial application is not allowed while using Function, Pierre Courtieu, 06/08/2015
- Re: [Coq-Club] Partial application is not allowed while using Function, Marcus Ramos, 06/09/2015
Archive powered by MHonArc 2.6.18.