Cyclic type definition in Coq

0
votes

I am trying to implement the following:

t ::= x | ( ) | case t of () | (t 1 , t 2) | pi_i t | in_i t | ... | suspend e

e ::= x | ( ) | (e 1 , e 2 ) | ... | t

Using inductives, t depends on e and vice versa. How can I implement it in Coq? I cannot use e when I haven't yet defined it.

1
coq

1 Answers

2
votes

Coq allows mutually inductive types:

Inductive t :=
  | Suspend : e -> t
  | ...
with e :=
  | T : t -> e
  | ...

See the reference manual for more details: https://coq.inria.fr/distrib/current/refman/language/cic.html#inductive-definitions