coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Partial application is not allowed while using Function
- Date: Sat, 6 Jun 2015 10:59:37 +0100
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.