coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
- To: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Recursive identify function
- Date: Tue, 1 May 2012 17:03:40 -0400
Hi, Jeffrey --
Coq has some special cases for list functions, so it turns out that this definition works:
Fixpoint h (c : C) : C :=
match c with
| Build_C x => Build_C (map h x)
end.
Hope this helps.
On Tue, May 1, 2012 at 4:37 PM, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:
Hi,
Given
Inductive C : Set :=Build_C : list C -> C.
how would you define a function with the same functionality as
Definition f (c : C) : C := cbut which constructed its return value recursively? Presumably Coq won't accept
Fixpoint h (l : list C) : list C :=
match l with |nil => nil |c :: l' => g c :: h l'endwith g (c : C) : C :=match c with |Build_C x => Build_C (h x)end.
because it cannot be sure that the function will terminate.
Thanks.
Regards,Jeff.
gregory malecha
- [Coq-Club] Recursive identify function, Terrell, Jeffrey
- Re: [Coq-Club] Recursive identify function, Gregory Malecha
- Re: [Coq-Club] Recursive identify function,
Terrell, Jeffrey
- Re: [Coq-Club] Recursive identify function,
Pierre Courtieu
- Re: [Coq-Club] Recursive identify function, Pierre Courtieu
- Re: [Coq-Club] Recursive identify function,
Pierre Courtieu
- Re: [Coq-Club] Recursive identify function,
Terrell, Jeffrey
- Re: [Coq-Club] Recursive identify function, Gregory Malecha
Archive powered by MhonArc 2.6.16.