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.