3.2.3.2.1. Level Expressions🔗

Levels that occur in a definition are not restricted to just variables and addition of constants. More complex relationships between universes can be defined using level expressions.

Level ::= 0 | 1 | 2 | ...  -- Concrete levels
        | u, v             -- Variables
        | Level + n        -- Addition of constants
        | max Level Level  -- Least upper bound
        | imax Level Level -- Impredicative LUB

Given an assignment of level variables to concrete numbers, evaluating these expressions follows the usual rules of arithmetic. The imax operation is defined as follows:

\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}

imax is used to implement impredicative quantification for Prop. In particular, if A : Sort u and B : Sort v, then (x : A) → B : Sort (imax u v). If B : Prop, then the function type is itself a Prop; otherwise, the function type's level is the maximum of u and v.

3.2.3.2.2. Universe Variable Bindings

Universe-polymorphic definitions bind universe variables. These bindings may be either explicit or implicit. Explicit universe variable binding and instantiation occurs as a suffix to the definition's name. Universe parameters are defined or provided by suffixing the name of a constant with a period (.) followed by a comma-separated sequence of universe variables between curly braces.

Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters. When the describe this option and add xref autoImplicit option is set to true (the default), it is not necessary to explicitly bind universe variables. When it is set to false, then they must be added explicitly or declared using the universe command. xref

unknown universe level 'u'

unknown universe level 'v'

In addition to using autoImplicit, particular identifiers can be declared as universe variables in a particular section scope using the universe command.

command ::= ...
    | Declares one or more universe variables.

`universe u v`

`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].

Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.

[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)

```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a

/- Implicit type-universe parameter, equivalent to `id₁`.
  Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a

/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```

On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.

```lean
def L₁.{u} := List (Type u)

-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`

universe u
def L₃ := List (Type u)
```

## Examples

```lean
universe u v w

structure Pair (α : Type u) (β : Type v) : Type (max u v) where
  a : α
  b : β

#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
universe ident ident*

Because the automatic implicit parameter feature only insert parameters that are used in the declaration's header, universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with universe even when autoImplicit is true.

unknown universe level 'u'

3.2.3.2.3. Universe Unification

3.2.3.2.4. Universe Lifting

PLift.{u} (α : Sort u) : Type u

ULift.{r, s} (α : Type s) : Type (max s r)

3.2.4.1.1. Parameters and Indices🔗

Type constructors may take two kinds of arguments: parameters and indices. Parameters must be used consistently in the entire definition; all occurrences of the type constructor in each constructor in the declaration must take precisely the same argument. Indices may vary among the occurrences of the type constructor. All parameters must precede all indices in the type constructor's signature.

Parameters that occur prior to the colon (':') in the type constructor's signature are considered parameters to the entire inductive type declaration. They are always parameters that must be uniform throughout the type's definition. Generally speaking, parameters that occur after the colon are indices that may vary throughout the definition of the type. However, if the option inductive.autoPromoteIndices is true, then syntactic indices that could have been parameters are made into parameters. An index could have been a parameter if all of its type dependencies are themselves parameters and it is used uniformly as an uninstantiated variable in all occurrences of the inductive type's type constructor in all constructors.

inductive.autoPromoteIndices

Indices can be seen as defining a family of types. Each choice of indices selects a type from the family, which has its own set of available constructors. Type constructors with indices are said to specify indexed families of types.

3.2.4.1.2. Example Inductive Types🔗

One : Type

One.one : One

Yes : Prop

Yes.intro : Yes

type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true : Type
but is expected to have type
  EvenOddList String true : Type

inductive datatype parameter mismatch
  α
expected
  α✝

3.2.4.1.3. Anonymous Constructor Syntax🔗

If an inductive type has just one constructor, then this constructor is eligible for anonymous constructor syntax. Instead of writing the constructor's name applied to its arguments, the explicit arguments can be enclosed in angle brackets ('⟨' and '⟩', Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) and MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)) and separated with commas. This works in both pattern and expression contexts. Providing arguments by name or converting all implicit parameters to explicit parameters with @ requires using the ordinary constructor syntax.

3.2.4.1.4. Deriving Instances🔗

The optional Lean.Parser.Command.inductive : commandderiving clause of an inductive type declaration can be used to derive instances of type classes. Please refer to the section on instance deriving for more information.

3.2.4.2.1. Structure Parameters🔗

Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe. Structures may not define indexed families.

3.2.4.2.2. Fields🔗

Each field of a structure declaration corresponds to a parameter of the constructor. Auto-implicit arguments are inserted in each field separately, even if their names coincide, and the fields become constructor parameters that quantify over types.

For each field, a projection function is generated that extracts the field's value from the underlying type's constructor. This function is in the structure's name's namespace. Structure field projections are handled specially by the elaborator (as described in the section on structure inheritance), which performs extra steps beyond looking up a namespace. When field types depend on prior fields, the types of the dependent projection functions are written in terms of earlier projections, rather than explicit pattern matching.

Structure fields may have default values, specified with :=. These values are used if no explicit value is provided.

Structure fields may additionally be accessed via their index, using dot notation. Fields are numbered beginning with 1.

3.2.4.2.3. Structure Constructors🔗

Structure constructors may be explicitly named by providing the constructor name and :: prior to the fields. If no name is explicitly provided, then the constructor is named mk in the structure type's namespace. Declaration modifiers may additionally be provided along with an explicit constructor name.

Because structures are represented by single-constructor inductive types, their constructors can be invoked or matched against using anonymous constructor syntax. Additionally, structures may be constructed or matched against using structure instance notation, which includes the names of the fields together with values for them.

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{ structInstField,*
        (: term)? }

structInstField ::= ...
    | structInstLVal := term

structInstField ::= ...
    | ident

false

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{term with
        structInstField,*
        (: term)?}

({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })

Values of structure types may also be declared using Lean.Parser.Command.declValEqns : commandwhere, followed by definitions for each field. This may only be used as part of a definition, not in an expression context.

3.2.4.2.4. Structure Inheritance🔗

Structures may be declared as extending other structures using the optional Lean.Parser.Command.structure : commandextends clause. The resulting structure type has all of the fields of all of the parent structure types. If the parent structure types have overlapping field names, then all overlapping field names must have the same type. If the overlapping fields have different default values, then the default value from the last parent structure that includes the field is used. New default values in the child structure take precedence over default values from the parent structures.

When the new structure extends existing structures, the new structure's constructor takes the existing structure's information as additional arguments. Typically, this is in the form of a constructor parameter for each parent structure type. If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead to prevent duplicating field information.

There is no subtyping relation between a parent structure type and its children. Even if structure B extends structure A, a function expecting an A will not accept a B. However, conversion functions are generated that convert a structure into each of its parents. These conversion functions are in the child structure's namespace, and their name is the parent structure's name preceded by to.

The resulting structure's projections can be used as if its fields are simply the union of the parents' fields. The Lean elaborator automatically generates an appropriate projection when fields are used. Likewise, the field-based initialization and structure update notations hide the details of the encoding of inheritance. The encoding is, however, visible when using the constructor's name, when using anonymous constructor syntax, or when referring to fields by their index rather than their name.

{ fst := 17, snd := 2 }

application type mismatch
  printEven two
argument
  two
has type
  EvenPrime : Type
but is expected to have type
  EvenNumber : Type

3.2.4.3.1. Recursors🔗

Every inductive type is equipped with a recursor. The recursor is completely determined by the signatures of the type constructor and the constructors. Recursors have function types, but they are primitive and are not definable using fun.

3.2.4.3.2. Well-Formedness Requirements🔗

Inductive type declarations are subject to a number of well-formedness requirements. These requirements ensure that Lean remains consistent as a logic when it is extended with the inductive type's new rules. They are conservative: there exist potential inductive types that do not undermine consistency, but that these requirements nonetheless reject.

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared

bootstrap.inductiveCheckResultingUniverse

invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
  Sort u
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.

3.2.4.3.3. Constructions for Termination Checking🔗

In addition to the type constructor, constructors, and recursors that Lean's core type theory prescribes for inductive types, Lean constructs a number of useful helpers. First, the equation compiler (which translates recursive functions with pattern matching in to applications of recursors) makes use of these additional constructs:

• recOn is a version of the recursor in which the target is prior to the cases for each constructor.

• casesOn is a version of the recursor in which the target is prior to the cases for each constructor, and recursive arguments do not yield induction hypotheses. It expresses case analysis rather than primitive recursion.

• below computes a type that, for some motive, expresses that all inhabitants of the inductive type that are subtrees of the target satisfy the motive. It transforms a motive for induction or primitive recursion into a motive for strong recursion or strong induction.

• brecOn is a version of the recursor in which below is used to provide access to all subtrees, rather than just immediate recursive parameters. It represents strong induction.

• noConfusion is a general statement from which injectivity and disjointness of constructors can be derived.

• noConfusionType is the motive used for noConfusion that determines what the consequences of two constructors being equal would be. For separate constructors, this is False; if both constructors are the same, then the consequence is the equality of their respective parameters.

For well-founded recursion, it is frequently useful to have a generic notion of size available. This is captured in the SizeOf class.

SizeOf.{u} (α : Sort u) : Sort (max 1 u)

3.2.4.4.1. Exceptions🔗

Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler:

• The fixed-width integer types UInt8, ..., UInt64, and USize are represented by the C types uint8_t, ..., uint64_t, and size_t, respectively.

• Char is represented by uint32_t

• Float is represented by double

• An enum inductive type of at least 2 and at most 2^{32} constructors, each of which has no parameters, is represented by the first type of uint8_t, uint16_t, uint32_t that is sufficient to assign a unique value to each constructor. For example, the type Bool is represented by uint8_t, with values 0 for false and 1 for true. Find out whether this should say "no relevant parameters"

• Decidable α is represented the same way as Bool Aren't Decidable and Bool just special cases of the rules for trivial constructors and irrelevance?

• Nat is represented by lean_object *. Its run-time value is either a pointer to an opaque arbitrary-precision integer object or, if the lowest bit of the “pointer” is 1 (checked by lean_is_scalar), an encoded unboxed natural number (lean_box/lean_unbox). Move these to FFI section or Nat chapter

3.2.4.4.2. Relevance🔗

Types and proofs have no run-time representation. That is, if an inductive type is a Prop, then its values are erased prior to compilation. Similarly, all theorem statements and types are erased. Types with run-time representations are called relevant, while types without run-time representations are called irrelevant.

In most cases, irrelevant values simply disappear from compiled code. However, in cases where some representation is required (such as when they are arguments to polymorphic constructors), they are represented by a trivial value.

3.2.4.4.3. Trivial Wrappers🔗

If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter.

3.2.4.4.4. Other Inductive Types🔗

If an inductive type doesn't fall into one of the categories above, then its representation is determined by its constructors. Constructors without relevant parameters are represented by their index into the list of constructors, as unboxed unsigned machine integers (scalars). Constructors with relevant parameters are represented as an object with a header, the constructor's index, an array of pointers to other objects, and then arrays of scalar fields sorted by their types. The header tracks the object's reference count and other necessary bookkeeping.

Recursive functions are compiled as they are in most programming languages, rather than by using the inductive type's recursor. Elaborating recursive functions to recursors serves to provide reliable termination evidence, not executable code.

3.2.4.5.1. Requirements🔗

The inductive types declared in a mutual block are considered as a group; they must collectively satisfy generalized versions of the well-formedness criteria for non-mutually-recursive inductive types. This is true even if they could be defined without the mutual block, because they are not in fact mutually recursive.

unknown identifier 'FreshList'

invalid inductive type, number of parameters mismatch in mutually inductive datatypes

invalid mutually inductive types, parameter 'α' has type
  Type u : Type (u + 1)
but is expected to have type
  Type : Type 1

invalid mutually inductive types, resulting universe mismatch, given
  Prop
expected type
  Type

(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared

3.2.4.5.2. Recursors🔗

Mutual inductive types are provided with primitive recursors, just like non-mutually-defined inductive types. These recursors take into account that they must process the other types in the group, and thus will have a motive for each inductive type. Because all inductive types in the mutual group are required to have identical parameters, the recursors still take the parameters first, abstracting them over the motives and the rest of the recursor. Additionally, because the recursor must process the group's other types, it will require cases for each constructor of each of the types in the group. The actual dependency structure between the types is not taken into account; even if an additional motive or constructor case is not really required due to there being fewer mutual dependencies than there could be, the generated recursor still requires them.

3.2.4.5.3. Run-Time Representation🔗

Mutual inductive types are represented identically to non-mutual inductive types in compiled code and in the runtime. The restrictions on mutual inductive types exist to ensure Lean's consistency as a logic, and do not impact compiled code.