How to define an inductive type and a definition at the same time?

Question

I want to have the following definitions:

Inductive a : Set :=
| basic : string -> a
| complex : string -> list t -> a.
The reference t was not found in the current
environment.

Definition t := string * a * a.
The reference a was not found in the current
environment.

As you can see, when defining a, t is used and when defining t, a is used. My question is how can I define these two at the same time?

Answer

You can define them mutually with the Inductive command.

Inductive a : Set :=
| basic : string -> a
| complex : string -> list t -> a
with t : Set :=
| t_intro : string * a * a -> t.

Or you can substitute using the definition of t, and define t afterwards.

Inductive a : Set :=
| basic : string -> a
| complex : string -> list (string * a * a) -> a.

Definition t : Set := (string * a * a)%type.

Definition complex' : string -> list t -> a := complex.