Data

See the official user manual for the most up-to-date version of the information on this page.

TOC

Data declarations include:

• inductive families, and,
• coinductive families.

The general format is:

data <name> <parameters> : <indices>

for the signature part of the declaration, and

data <name> where
  <constructor> : <term>
  ...

for the definition part. A data signature immediately followed by its definition may be abbreviated by the following.

data <name> <parameters> : <indices> where
  <constructor> : <term>
  ...

<name> is a new unqualified name, the name being declared.

<parameters> is an optional telescope. This specifies arguments to <name> that do not vary in the types of the constructors. Variables introduced in <parameters> are in scope for the indices and all the constructor lines.

<indices> is a term denoting a function space whose innermost range is a universe. This specifies remaining arguments to <name>, which are called indices and may vary in the types of the constructors, and the result type (the universe). Variables introduced in <indices> are in scope for the indices only.

There may be zero or more <constructor> lines. Each <constructor> is an unqualified name. It need not be new: constructors can be overloaded. The <term> following a constructor is a term denoting a function space whose innermost range is a full application of <name>.