I had been trying to make function whose return type is dependent on a list.

Like this:

```
Require Import List.
Import ListNotations.
Inductive enum (A: Type): list A -> Type :=
| Zero: forall ls:list A,
enum A ls
| More: forall (ls:list A) (a:A),
enum A (a::ls).
Fixpoint foo (n:nat): forall ls:list nat, enum nat ls :=
match n with
| O => fun ls => Zero _ ls
| S n' => fun ls => (* More _ ls n' *)
end.
(*
In environment
foo : nat -> forall ls : list nat, enum nat ls
n : nat
n' : nat
ls : list nat
The term "More nat ls n'" has type "enum nat (n' :: ls)"
while it is expected to have type "enum nat ls".
*)
```

But couldn't do it.

How can such a function be defined?

The return type is dependent on a list which won't be same for all possible constructors.

The return type of `foo`

states that it will return an `enum`

for any `n: nat`

and `ls : list nat`

, while your comment seem to indicate that you have a specific list in mind (possibly defined using `n : nat`

). Is this really the type you want to inhabit ?

this `foo`

compiles.. but I'm not sure it is what you would like to have in result.

```
Fixpoint foo (n:nat): forall ls:list nat,
match n with O => enum nat ls | S n' => enum nat (n'::ls) end
:=
match n with
| O => fun ls => Zero _ ls
| S n' => fun ls => More _ ls n'
end.
```

Kenji Maillard said:

Is this really the type you want to inhabit ?

I wasn't sure if that's how the type should be stated, to be honest..

I have a type depedent on a list. While values of this type are being built, the list changes. And this causes a type mismatch.

I wanted to skirt around this problem.

That's what I wanted to show with this example. Not sure how well I expressed it..

Andrey Klaus said:

this

`foo`

compiles.. but I'm not sure it is what you would like to have in result.`Fixpoint foo (n:nat): forall ls:list nat, match n with O => enum nat ls | S n' => enum nat (n'::ls) end := match n with | O => fun ls => Zero _ ls | S n' => fun ls => More _ ls n' end.`

Is it possible to use the `foo`

as a recursive call inside the first `match`

as well?

Julin Shaji said:

Is it possible to use the

`foo`

as a recursive call inside the first`match`

as well?

I do not think so. What problem do you try to solve?

You cannot use `foo`

in its own type but you could first define the list employed in the type of `foo`

by induction on `n:nat`

and then implement a variant of `foo`

:

```
Fixpoint downToZero (n : nat) : list nat :=
match n with
| 0 => []
| S n => n :: downToZero n
end.
Definition foo (n : nat) : enum nat (downToZero n) :=
match n as k return enum nat (downToZero k) with
| 0 => Zero nat []
| S n => More nat (downToZero n) n
end.
```

By the way, if you want `enum`

to actually enumerate/frame a prefix of your list, you should probably have a recursive occurence in the constructor `More`

, e.g.:

```
Inductive enum (A: Type): list A -> Type :=
| Zero: forall ls:list A,
enum A ls
| More: forall (ls:list A) (a:A), enum A ls ->
enum A (a::ls).
```

Last updated: Jun 13 2024 at 21:01 UTC