CODEWITHSUNDEEP
coq
Lisa
Lisa

Reputation: 227

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

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!

Upvotes: 2

Views: 235

Answers (1)

user3551663
user3551663

Reputation:

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.

Upvotes: 4

Related Questions