Определение типов пересечений в Coq

Question

Я пытаюсь определить версию простейшего лямбда-исчисления плюс типы пересечений. Я попробовал следующее:

Inductive ty : Type :=
| Bool : ty
| Int : ty
| Arrow: ty -> ty -> ty
| Inters: ty ?? ty.

Кажется, я мог только добавить "->". В противном случае я получаю ошибку. Как я могу добавить новый конструктор?

Answer 1

Вы хотите что-то вроде:

Inductive ty : Type :=
| Bool : ty
| Int : ty
| Arrow: ty -> ty -> ty
| Inters: ty -> ty -> ty.