The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 08/01/2014 16:41, Terrell, Jeffrey wrote:
> 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.

Hi,

No, currently you can't. Nested inductive types require nested fix and
mutual inductive types require mutual fix. All you can do is write g
parameterized by h, before the mutual f and h.

Given the trouble we're having these days with the guard condition, it
is not sure we are going to consider more extensions before a thorough
check that it's OK, although the fix candidate is doing a significant
step towards allowing it.

Bruno.