Search code examples
coq

Defining intersection types in Coq

I am trying to define a version of the simply typed lambda calculus plus intersection types. I tried the following:

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

It seems that I could only add "->". Otherwise, I get a bug. How could I add a new constructor?

Solution

  • You want something such as:

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