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.

Definition t := string * a * a. 

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?

Thanks a lot!

Answer 1

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.