The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

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.