The Coq mailing list

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

Hi,

It is possible to reorganise the following example (which is not meant to do 
anything useful) so that the definition of g is not contained within f?

Inductive A : Set :=
   Build_A : list B -> A
with B : Set :=
   Build_B : A -> B.

Fixpoint f (a : A ) : list B :=
   match a with Build_A l =>
      (fix g (l : list B) : list B :=
         match l with
            nil => nil |
            b :: l' => b :: g l' ++ h b
         end) l
   end
with h (b : B) : list B :=
   match b with Build_B a =>
      f a
   end.

Thanks.

Regards,
Jeff.