3.7.1.1. Sum Types as Classes🔗

Most type classes follow the paradigm of a set of overloaded methods from which clients may choose freely. This is naturally modeled by a product type, from which the overloaded methods are projections. Some classes, however, are sum types: they require that the recipient of the synthesized instance first check which of the available instance constructors was provided. To account for these classes, a class declaration may consist of an arbitrary inductive type, not just an extended form of structure declaration.

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      class inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

Class inductive types are just like other inductive types, except they may participate in instance synthesis. The paradigmatic example of a class inductive is Decidable: synthesizing an instance in a context with free variables amounts to synthesizing the decision procedure, but if there are no free variables, then the truth of the proposition can be established by instance synthesis alone (as is done by the decide tactic).

3.7.1.2. Class Abbreviations🔗

In some cases, many related type classes may co-occur throughout a codebase. Rather than writing all the names repeatedly, it would be possible to define a class that extends all the classes in question, contributing no new methods itself. However, this new class has a disadvantage: its instances must be declared explicitly.

The Lean.Parser.Command.classAbbrev : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ``` class abbrev command allows the creation of class abbreviations in which one name is short for a number of other class parameters. Behind the scenes, a class abbreviation is represented by a class that extends all the others. Its constructor is additionally declared to be an instance so the new class can be constructed by instance synthesis alone.

37

failed to synthesize
  AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.

37

3.7.2.1. Recursive Instances🔗

Functions defined in Lean.Parser.Command.declaration : commandwhere structure definition syntax are not recursive. Because instance declaration is a version of structure definition, type class methods are also not recursive by default. Instances for recursive inductive types are common, however. There is a standard idiom to work around this limitation: define a recursive function independently of the instance, and then refer to it in the instance definition. By convention, these recursive functions have the name of the corresponding method, but are defined in the type's namespace.

failed to synthesize
  BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Furthermore, instances are not available for instance synthesis during their own definitions. They are first marked as being available for instance synthesis after they are defined. Nested inductive types, in which the recursive occurrence of the type occurs as a parameter to some other inductive type, may require an instance to be available to write even the recursive function. The standard idiom to work around this limitation is to create a local instance in a recursively-defined function that includes a reference to the function being defined, taking advantage of the fact that instance synthesis may use every binding in the local context with the right type.

failed to synthesize
  BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.7.2.2. Instances of class inductives🔗

Many instances have function types: any instance that itself recursively invokes instance search is a function, as is any instance with implicit parameters. While most instances only project method implementations from their own instance parameters, instances of class inductive types typically pattern-match one or more of their arguments, allowing the instance to select the appropriate constructor. This is done using ordinary Lean function syntax. Just as with other instances, the function in question is not available for instance synthesis in its own definition.

failed to synthesize
  Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.7.2.3. Instance Priorities🔗

Instances may be assigned priorities. During instance synthesis, higher-priority instances are preferred; see the section on instance synthesis for details of instance synthesis.

prio ::=
    num

prio ::= ...
    | The default priority `default = 1000`, which is used when no priority is set. default

prio ::= ...
    | The standardized "low" priority `low = 100`, for things that should be lower than default priority. low

prio ::= ...
    | The standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.
mid

prio ::= ...
    | The standardized "high" priority `high = 10000`, for things that should be higher than default priority. high

prio ::= ...
    | Parentheses are used for grouping priority expressions. (prio)

prio ::= ...
    | Addition of priorities. This is normally used only for offsetting, e.g. `default + 1`. prio + prio

prio ::= ...
    | Subtraction of priorities. This is normally used only for offsetting, e.g. `default - 1`. prio - prio

3.7.2.4. Default Instances🔗

The default_instance attribute specifies that an instance should be used as a fallback in situations where there is not enough information to select it otherwise. If no priority is specified, then the default priority default is used.

attr ::= ...
    | default_instance prio?

{ half := 0 }

{ half := 17 }

{ half := 127 }

{ half := 0 }

{ half := 17 }

5

3.7.2.5. The Instance Attribute🔗

The instance attribute declares a name to be an instance, with the specified priority. Like other attributes, instance can be applied globally, locally, or only when the current namespace is opened. The Lean.Parser.Command.declaration : commandinstance declaration is a form of definition that automatically applies the instance attribute.

attr ::= ...
    | instance prio?

3.7.3.1. Instance Search Summary

Generally speaking, instance synthesis is a recursive search procedure that may, in general, backtrack arbitrarily. Synthesis may succeed with an instance term, fail if no such term can be found, or get stuck if there is insufficient information. A detailed description of the instance synthesis algorithm is available in Selsam, Ullrich, and de Moura (2020)Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura, 2020. “Tabled typeclass resolution”. arXiv:2001.04301. An instance search problem is given by a type class applied to concrete arguments; these argument values may or may not be known. Instance search attempts every locally-bound variable whose type is a class, as well as each registered instance, in order of priority and definition. When candidate instances themselves have instance-implicit parameters, they impose further synthesis tasks.

A problem is only attempted when all of the input parameters to the type class are known. When a problem cannot yet be attempted, then that branch is stuck; progress in other subproblems may result in the problem becoming solvable. Output or semi-output parameters may be either known or unknown at the start of instance search. Output parameters are ignored when checking whether an instance matches the problem, while semi-output parameters are considered.

Every candidate solution for a given problem is saved in a table; this prevents infinite regress in case of cycles as well as exponential search overheads in the presence of diamonds (that is, multiple paths by which the same goal can be achieved). A branch of the search fails when any of the following occur:

• All potential instances have been attempted, and the search space is exhausted.

• The instance size limit specified by the option synthInstance.maxSize is reached.

• The synthesized value of an output parameter does not match the specified value in the search problem. Failed branches are not retried.

If search would otherwise fail or get stuck, the search process attempts to use matching default instances in order of priority. For default instances, the input parameters do not need to be fully known, and may be instantiated by the instances parameter values. Default instances may take instance-implicit parameters, which induce further recursive search.

Successful branches in which the problem is fully known (that is, in which there are no unsolved metavariables) are pruned, and further potentially-successful instances are not attempted, because no later instance could cause the previously-succeeding branch to fail.

3.7.3.2. Instance Search Problems

Instance search occurs during the elaboration of (potentially nullary) function applications. Some of the implicit parameters' values are forced by others; for instance, an implicit type parameter may be solved using the type of a later value argument that is explicitly provided. Implicit parameters may also be solved using information from the expected type at that point in the program. The search for instance implicit arguments may make use of the implicit argument values that have been found, and may additionally solve others.

Instance synthesis begins with the type of the instance-implicit parameter. This type must be the application of a type class to zero or more arguments; these argument values may be known or unknown when search begins. If an argument to a class is unknown, the search process will not instantiate it unless the corresponding parameter is marked as an output parameter, explicitly making it an output of the instance synthesis routine.

Search may succeed, fail, or get stuck; a stuck search may occur when an unknown argument value becoming known might enable progress to be made. Stuck searches may be re-invoked when the elaborator has discovered one of the previously-unknown implicit arguments. If this does not occur, stuck searches become failures.

3.7.3.3. Candidate Instances

Instance synthesis uses both local and global instances in its search. Local instances are those available in the local context; they may be either parameters to a function or locally defined with let. Local instances do not need to be indicated specially; any local variable whose type is a type class is a candidate for instance synthesis. Global instances are those available in the global environment; every global instance is a defined name with the instance attribute applied.Lean.Parser.Command.declaration : commandinstance declarations automatically apply the instance attribute.

{ x := 0, y := 0 }

3.7.3.4. Instance Parameters and Synthesis🔗

The search process for instances is largely governed by class parameters. Type classes take a certain number of parameters, and instances are tried during the search when their choice of parameters is compatible with those in the class type for which the instance is being synthesized.

Instances themselves may also take parameters, but the role of instances' parameters in instance synthesis is very different. Instances' parameters represent either variables that may be instantiated by instance synthesis or further synthesis work to be done before the instance can be used. In particular, parameters to instances may be explicit, implicit, or instance-implicit. If they are instance implicit, then they induce further recursive instance searching, while explicit or implicit parameters must be solved by unification.

@aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)

3.7.3.5. Output Parameters🔗

By default, the parameters of a type class are considered to be inputs to the search process. If the parameters are not known, then the search process gets stuck, because choosing an instance would require the parameters to have values that match those in the instance, which cannot be determined on the basis of incomplete information. In most cases, guessing instances would make instance synthesis unpredictable.

In some cases, however, the choice of one parameter should cause an automatic choice of another. For example, the overloaded membership predicate type class Membership treats the type of elements of a data structure as an output, so that the type of element can be determined by the type of data structure at a use site, instead of requiring that there be sufficient type annotations to determine both types prior to starting instance synthesis. An element of a List Nat can be concluded to be a Nat simply on the basis of its membership in the list.

Type class parameters can be declared as outputs by wrapping their types in the outParam gadget. When a class parameter is an output, instance synthesis will not require that it be known; in fact, any existing value is ignored completely. The first instance that matches the input parameters is selected, and that instance's assignment of the output parameter becomes its value. If there was a pre-existing value, then it is compared with the assignment after synthesis is complete, and it is an error if they do not match.

outParam.{u} (α : Sort u) : Sort u

class Membership (α : outParam (Type u)) (γ : Type v)

typeclass instance problem is stuck, it is often due to metavariables
  Serialize (Nat × Nat) ?m.16

failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Semi-output parameters are like output parameters in that they are not required to be known prior to synthesis commencing; unlike output parameters, their values are taken into account when selecting instances.

semiOutParam.{u} (α : Sort u) : Sort u

class Coe (α : semiOutParam (Sort u)) (β : Sort v)

Semi-output parameters impose a requirement on instances: each instance of a class with semi-output parameters should determine the values of its semi-output parameters.

OneSmaller.shrink (some false) ⋯ : Bool

3.7.3.6. Default Instances🔗

When instance synthesis would otherwise fail, having not selected an instance, the default instances specified using the default_instance attribute are attempted in order of priority. When priorities are equal, more recently-defined default instances are chosen before earlier ones. The first default instance that causes the search to succeed is chosen.

Default instances may induce further recursive instance search if the default instances themselves have instance-implicit parameters. If the recursive search fails, the search process backtracks and the next default instance is tried.

3.7.3.7. “Morally Canonical” Instances

During instance synthesis, if a goal is fully known (that is, contains no metavariables) and search succeeds, no further instances will be attempted for that same goal. In other words, when search succeeds for a goal in a way that can't be refuted by a subsequent increase in information, the goal will not be attempted again, even if there are other instances that could potentially have been used. This optimization can prevent a failure in a later branch of an instance synthesis search from causing spurious backtracking that replaces a fast solution from an earlier branch with a slow exploration of a large state space.

The optimization relies on the assumption that instances are morally canonical. Even if there is more than one potential implementation of a given type class's overloaded operations, or more than one way to synthesize an instance due to diamonds, any discovered instance should be considered as good as any other. In other words, there's no need to consider all potential instances so long as one of them has been guaranteed to work. The optimization may be disabled with the backwards-compatibility option backward.synthInstance.canonInstances, which may be removed in a future version of Lean.

Code that uses instance-implicit parameters should be prepared to consider all instances as equivalent. In other words, it should be robust in the face of differences in synthesized instances. When the code relies on instances in fact being equivalent, it should either explicitly manipulate instances (e.g. via local definitions, by saving them in structure fields, or having a structure inherit from the appropriate class) or it should make this dependency explicit in the type, so that different choices of instance lead to incompatible types.

3.7.3.8. Options

backward.synthInstance.canonInstances

synthInstance.maxHeartbeats

synthInstance.maxSize

3.7.4.1. Deriving Handlers🔗

Instance deriving uses a table of deriving handlers that maps type class names to metaprograms that derive instances for them. Deriving handlers may be added to the table using registerDerivingHandler, which should be called in an Lean.Parser.Command.initialize : commandinitialize block. Each deriving handler should have the type Array Name → CommandElabM Bool. When a user requests that an instance of a class be derived, its registered handlers are called one at a time. They are provided with all of the names in the mutual block for which the instance is to be derived, and should either correctly derive an instance and return true or have no effect and return false. When a handler returns true, no further handlers are called.

Lean includes deriving handlers for the following classes:

• BEq

• DecidableEq

• Hashable

• Inhabited

• Nonempty

• Ord

• Repr

• SizeOf

• TypeName

Lean.Elab.registerDerivingHandler
    (className : Name)
    (handler : DerivingHandler) : IO Unit

3.7.5.1. Boolean Equality Tests

BEq.{u} (α : Type u) : Type u

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

LawfulBEq.{u} (α : Type u) [BEq α] : Prop

3.7.5.2. Ordering

Ord.{u} (α : Type u) : Type u

LT.{u} (α : Type u) : Type u

LE.{u} (α : Type u) : Type u

3.7.5.3. Decidability

A proposition is decidable if it can be checked algorithmically. The Law of the Excluded Middle means that every proposition is true or false, but it provides no way to check which of the two cases holds, which can often be useful. By default, only algorithmic Decidable instances for which code can be generated are in scope; opening the Classical namespace makes every proposition decidable.

Decidable (p : Prop) : Type

DecidableRel.{u} {α : Sort u} (r : α → α → Prop)
    : Sort (max 1 u)

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

Decidable.decide (p : Prop) [h : Decidable p] :
  Bool

Decidable.byCases.{u} {p : Prop} {q : Sort u}
  [dec : Decidable p] (h1 : p → q)
  (h2 : ¬p → q) : q

failed to synthesize
  Decidable (f = g)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.7.5.4. Inhabited Types

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

Nonempty.{u} (α : Sort u) : Prop

3.7.5.5. Visible Representations

Repr.{u} (α : Type u) : Type u

ToString.{u} (α : Type u) : Type u

3.7.5.6. Arithmetic and Bitwise Operators

Zero.{u} (α : Type u) : Type u

NeZero.{u_1} {R : Type u_1} [Zero R] (n : R)
    : Prop

HAdd.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Add.{u} (α : Type u) : Type u

HSub.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Sub.{u} (α : Type u) : Type u

HMul.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Mul.{u} (α : Type u) : Type u

HDiv.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Div.{u} (α : Type u) : Type u

Dvd.{u_1} (α : Type u_1) : Type u_1

HMod.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Mod.{u} (α : Type u) : Type u

HPow.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Pow.{u, v} (α : Type u) (β : Type v)
    : Type (max u v)

NatPow.{u} (α : Type u) : Type u

HomogeneousPow.{u} (α : Type u) : Type u

HShiftLeft.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

ShiftLeft.{u} (α : Type u) : Type u

HShiftRight.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

ShiftRight.{u} (α : Type u) : Type u

Neg.{u} (α : Type u) : Type u

HAnd.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

HOr.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

HXor.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

3.7.5.7. Append

HAppend.{u, v, w} (α : Type u) (β : Type v)
    (γ : outParam (Type w))
    : Type (max (max u v) w)

Append.{u} (α : Type u) : Type u