Declaring New Types

In Lean's library, every concrete type other than the universes and every type constructor other than the dependent function type is an instance of a general family of type constructions known as inductive types. It is remarkable that it is possible to develop complex programs and formalize mathematics based on nothing more than the type universes, dependent function types, and inductive types; everything else follows from those.

Intuitively, an inductive type is built up from a specified list of constructors. In Lean, the basic syntax for specifying such a type is as follows:

inductive NewType where
  | constructor_1 : ... → NewType
  | constructor_2 : ... → NewType
  | constructor_n : ... → NewType

The intuition is that each constructor specifies a way of building new objects of NewType, possibly from previously constructed values. The type NewType consists of nothing more than the objects that are constructed in this way.

We will see below that the arguments to the constructors can include objects of type NewType, subject to a certain "positivity" constraint, which guarantees that elements of NewType are built from the bottom up. Roughly speaking, each ... can be any function type constructed from NewType and previously defined types, in which NewType appears, if at all, only as the "target" of the function type.

We will provide a number of examples of inductive types. We will also consider slight generalizations of the scheme above, to mutually defined inductive types, and so-called inductive families.

Every inductive type comes with constructors, which show how to construct an element of the type, and elimination rules, which show how to "use" an element of the type in another construction.