The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

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 := c

but 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'

   end

with 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

http://www.people.fas.harvard.edu/~gmalecha/