I know that is possible to create mutually defined inductive types like tree and forest:

```
Parameters A B : Set.
Inductive tree : Set := node : A -> forest -> tree
with forest : Set :=
| leaf : B -> forest
| cons : tree -> forest -> forest.
```

is it possible to do something like that but using a fixpoint? For example:

```
Inductive Foo: Type :=
| cons1 : Foo
| cons2 : forall A B, fxpnt A B -> Foo
with fxpnt A B : Prop :=
...
```

I need to try that because the `fxpnt`

definition depends on the inductive and the other way around.

That sounds like induction-recursion, which is not supported in Coq.

One way to cheat your way out of this is to replace the fixpoint by an indexed inductive definition (basically, its graph). You lose computation, but this you can do in Coq.

```
Inductive Foo: Type :=
| cons1 : Foo
| cons2 : forall A B T, fxpnt A B T -> Foo
with fxpnt A B : Type -> Prop :=
...
```

that depends on how the fixpoint dependes on Foo

for instance if A or B is in Foo you need induction-induction

Last updated: Oct 01 2023 at 18:01 UTC