How to define an inductive type mutually recursive with a function?

Question

I want to define an inductive type Foo, with constructors accepting as arguments some properties. I want those properties to depend on inductive arguments of the type I am currently defining. I want to be able to collect some data from them inside those properties using some recursive function bar that would take an object of type Foo. However, I don't know of a way to declare those two so that Coq would accept their definitions. I want to be able to write something like this:

Inductive Foo : Set (* or Type *) :=
| Foo1 : forall f : Foo, bar f = 1 -> Foo
| Foo2 : forall f : Foo,  bar f = 2 -> Foo
| Foon : nat -> Foo
with bar (f : Foo) : nat := 
  match f with
  | Foo1 _ _ => 1
  | Foo2 _ _ => 2
  | Foon n => S n
  end.

Usually, with is the way to handle mutual recursion, however all examples I've seen was it being used with both definitions begin either both Inductive or both Fixpoint. Is such mutual recursion even possible?

Answer 1

This type of definition is known as an "inductive-recursive". It is not supported in Coq, unfortunately, but it is supported in the Agda theorem prover, if I am not mistaken.