3.7. Type Classes🔗

An operation is polymorphic if it can be used with multiple types. In Lean, polymorphism comes in three varieties:

  1. universe polymorphism, where the sorts in a definition can be instantiated in various ways,

  2. functions that take types as (potentially implicit) parameters, allowing a single body of code to work with any type, and

  3. ad-hoc polymorphism, implemented with type classes, in which operations to be overloaded may have different implementations for different types.

Because Lean does not allow case analysis of types, polymorphic functions implement operations that are uniform for any choice of type argument; for example, List.map does not suddenly compute differently depending on whether the input list contains Strings or Nats. Ad-hoc polymorphic operations are useful when there is no “uniform” way to implement an operation; the canonical use case is for overloading arithmetic operators so that they work with Nat, Int, Float, and any other type that has a sensible notion of addition. Ad-hoc polymorphism may also involve multiple types; looking up a value at a given index in a collection involves the collection type, the index type, and the type of member elements to be extracted. A type classType classes were first described in Philip Wadler and Stephen Blott, 1980. “How to make ad-hoc polymorphism less ad hoc”. In Proceedings of the 16th Symposium on Principles of Programming Languages. describes a collection of overloaded operations (called methods) together with the involved types.

Type classes are very flexible. Overloading may involve multiple types; operations like indexing into a data structure can be overloaded for a specific choice of data structure, index type, element type, and even a predicate that asserts the presence of the key in the structure. Due to Lean's expressive type system, overloading operations is not restricted only to types; type classes may be parameterized by ordinary values, by families of types, and even by predicates or propositions. All of these possibilities are used in practice:

Natural number literals

The OfNat type class is used to interpret natural number literals. Instances may depend not only on the type being instantiated, but also on the number literal itself.

Computational effects

Type classes such as Monad, whose parameter is a function from one type to another, are used to provide special syntax for programs with side effects. The “type” for which operations are overloaded is actually a type-level function, such as Option, IO, or Except.

Predicates and propositions

The Decidable type class allows a decision procedure for a proposition to be found automatically by Lean. This is used as the basis for termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if-expressions, which may branch on any decidable proposition.

While ordinary polymorphic definitions simply expect instantiation with arbitrary parameters, the operators overloaded with type classes are to be instantiated with instances that define the overloaded operation for some specific set of parameters. These instance-implicit parameters are indicated in square brackets. At invocation sites, Lean either synthesizes a suitable instance from the available candidates or signals an error. Because instances may themselves have instance parameters, this search process may be recursive and result in a final composite instance value that combines code from a variety of instances. Thus, type class instance synthesis is also a means of constructing programs in a type-directed manner.

Here are some typical use cases for type classes:

  • Type classes may represent overloaded operators, such as arithmetic that can be used with a variety of types of numbers or a membership predicate that can be used for a variety of data structures. There is often a single canonical choice of operator for a given type—after all, there is no sensible alternative definition of addition for Nat—but this is not an essential property, and libraries may provide alternative instances if needed.

  • Type classes can represent an algebraic structure, providing both the extra structure and the axioms required by the structure. For example, a type class that represents an Abelian group may contain methods for a binary operator, a unary inverse operator, an identity element, as well as proofs that the binary operator is associative and commutative, that the identity is an identity, and that the inverse operator yields the identity element on both sides of the operator. Here, there may not be a canonical choice of structure, and a library may provide many ways to instantiate a given set of axioms; there are two equally canonical monoid structures over the integers.

  • A type class can represent a relation between two types that allows them to be used together in some novel way by a library. The Coe class represents automatically-inserted coercions from one type to another, and MonadLift represents a way to run operations with one kind of effect in a context that expects another kind.

  • Type classes can represent a framework of type-driven code generation, where instances for polymorphic types each contribute some portion of a final program. The Repr class defines a canonical pretty printer for a type, and polymorphic types end up with polymorphic Repr instances. When pretty printing is finally invoked on an expression with a known concrete type, such as List (Nat × (String ⊕ Int)), the resulting pretty printer contains code assembled from the Repr instances for List, Prod, Nat, Sum, String, and Int.

3.7.1. Class Declarations🔗

Type classes are declared with the Lean.Parser.Command.declaration : commandclass keyword.

The Lean.Parser.Command.declaration : commandclass declaration creates a new single-constructor inductive type, just as if the Lean.Parser.Command.declaration : commandstructure command had been used instead. In fact, the results of the Lean.Parser.Command.declaration : commandclass and Lean.Parser.Command.declaration : commandstructure commands are almost identical, and features such as default values may be used the same way in both. Please refer to the documentation for structures for more information about default values, inheritance, and other features of structures. The differences between structure and class declarations are:

Methods instead of fields

Instead of creating field projections that take a value of the structure type as an explicit parameter, methods are created. Each method takes the corresponding instance as an instance-implicit parameter.

Instance-implicit parent classes

The constructor of a class that extends other classes takes its class parents' instances as instance-implicit parameters, rather than explicit parameters. When instances of this class are defined, instance synthesis is used to find the values of inherited fields. Parents that are not classes are still explicit parameters to the underlying constructor.

Parent projections via instance synthesis

Structure field projections make use of inheritance information to project parent structure fields from child structure values. Classes instead use instance synthesis: given a child class instance, synthesis will construct the parent; thus, methods are not added to child classes in the same way that projections are added to child structures.

Registered as class

The resulting inductive type is registered as a type class, for which instances may be defined and that may be used as the type of instance-implicit arguments.

Out and semi-out parameters are considered

The outParam and semiOutParam gadgets have no meaning in structure definitions, but they are used in class definitions to control instance search.

While Lean.Parser.Command.declaration : commandderiving clauses are allowed for class definitions to maintain the parallel between class and structure elaboration, they are not frequently used and should be considered an advanced feature.

No Instances of Non-Classes

Lean rejects instance-implicit parameters of types that are not classes:

def f [n : invalid binder annotation, type is not a class instance Nat use the command `set_option checkBinderAnnotations false` to disable the checkNat] : n = n := rfl 
invalid binder annotation, type is not a class instance
  Nat
use the command `set_option checkBinderAnnotations false` to disable the check
Class vs Structure Constructors

A very small algebraic hierarchy can be represented either as structures (S.Magma, S.Semigroup, and S.Monoid below), a mix of structures and classes (C1.Monoid), or only using classes (C2.Magma, C2.Semigroup, and C2.Monoid):

namespace S structure Magma (α : Type u) where op : α → α → α structure Semigroup (α : Type u) extends Magma α where op_assoc : ∀ x y z, op (op x y) z = op x (op y z) structure Monoid (α : Type u) extends Semigroup α where ident : α ident_left : ∀ x, op ident x = x ident_right : ∀ x, op x ident = x end S namespace C1 class Monoid (α : Type u) extends S.Semigroup α where ident : α ident_left : ∀ x, op ident x = x ident_right : ∀ x, op x ident = x end C1 namespace C2 class Magma (α : Type u) where op : α → α → α class Semigroup (α : Type u) extends Magma α where op_assoc : ∀ x y z, op (op x y) z = op x (op y z) class Monoid (α : Type u) extends Semigroup α where ident : α ident_left : ∀ x, op ident x = x ident_right : ∀ x, op x ident = x end C2

S.Monoid.mk and C1.Monoid.mk have identical signatures, because the parent of the class C1.Monoid is not itself a class:

S.Monoid.mk.{u} {α : Type u} (toSemigroup : S.Semigroup α) (ident : α) (ident_left : ∀ (x : α), toSemigroup.op ident x = x) (ident_right : ∀ (x : α), toSemigroup.op x ident = x) : S.Monoid αC1.Monoid.mk.{u} {α : Type u} (toSemigroup : S.Semigroup α) (ident : α) (ident_left : ∀ (x : α), toSemigroup.op ident x = x) (ident_right : ∀ (x : α), toSemigroup.op x ident = x) : C1.Monoid α

Similarly, because neither S.Magma nor C2.Magma inherits from another structure or class, their constructors are identical:

S.Magma.mk.{u} {α : Type u} (op : α → α → α) : S.Magma αC2.Magma.mk.{u} {α : Type u} (op : α → α → α) : C2.Magma α

S.Semigroup.mk, however, takes its parent as an ordinary parameter, while C2.Semigroup.mk takes its parent as an instance implicit parameter:

S.Semigroup.mk.{u} {α : Type u} (toMagma : S.Magma α) (op_assoc : ∀ (x y z : α), toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) : S.Semigroup αC2.Semigroup.mk.{u} {α : Type u} [toMagma : C2.Magma α] (op_assoc : ∀ (x y z : α), toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) : C2.Semigroup α

Finally, C2.Monoid.mk takes its semigroup parent as an instance implicit parameter. The references to op become references to the method C2.Magma.op, relying on instance synthesis to recover the implementation from the C2.Semigroup instance-implicit parameter via its parent projection:

C2.Monoid.mk.{u} {α : Type u} [toSemigroup : C2.Semigroup α] (ident : α) (ident_left : ∀ (x : α), C2.Magma.op ident x = x) (ident_right : ∀ (x : α), C2.Magma.op x ident = x) : C2.Monoid α

Parameters to type classes may be marked with gadgets, which are special versions of the identity function that cause the elaborator to treat a value differently. Gadgets never change the meaning of a term, but they may cause it to be treated differently in elaboration-time search procedures. The gadgets outParam and semiOutParam affect instance synthesis, so they are documented in that section.

Whether a type is a class or not has no effect on definitional equality. Two instances of the same class with the same parameters are not necessarily identical and may in fact be very different.

Instances are Not Unique

This implementation of binary heap insertion is buggy:

structure Heap (α : Type u) where contents : Array α deriving Repr def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α := if h : i = 0 then xs else if h : i ≥ xs.contents.size then xs else let j := i / 2 if Ord.compare xs.contents[i] xs.contents[j] == .lt then Heap.bubbleUp j {xs with contents := α:Type ?u.802inst✝:Ord αi:Natxs:Heap αh✝:¬i = 0h:¬i ≥ xs.contents.sizej:Nat := i / 2⊢ sorry < xs.contents.size invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨j, by omega⟩} else xs def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α := let i := xs.contents.size {xs with contents := xs.contents.push x}.bubbleUp i

The problem is that a heap constructed with one Ord instance may later be used with another, leading to the breaking of the heap invariant.

One way to correct this is to making the heap type depend on the selected Ord instance:

structure Heap' (α : Type u) [Ord α] where contents : Array α def Heap'.bubbleUp [inst : Ord α] (i : Nat) (xs : @Heap' α inst) : @Heap' α inst := if h : i = 0 then xs else if h : i ≥ xs.contents.size then xs else let j := i / 2 if inst.compare xs.contents[i] xs.contents[j] == .lt then Heap'.bubbleUp j {xs with contents := α:Type ?u.327inst:Ord αi:Natxs:Heap' αh✝:¬i = 0h:¬i ≥ xs.contents.sizej:Nat := i / 2⊢ sorry < xs.contents.size invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨j, by omega⟩} else xs def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α := let i := xs.contents.size {xs with contents := xs.contents.push x}.bubbleUp i invalid 'end', insufficient scopesend A

In the improved definitions, Heap'.bubbleUp is needlessly explicit; the instance does not need to be explicitly named here because Lean would select the indicated instances nonetheless, but it does bring the correctness invariant front and center for readers.

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.

syntax
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.

Class Abbreviations

Both plusTimes1 and plusTimes2 require that their parameters' type have Add and Mul instances:

class abbrev AddMul (α : Type u) := Add α, Mul α def plusTimes1 [AddMul α] (x y z : α) := x + y * z class AddMul' (α : Type u) extends Add α, Mul α def plusTimes2 [AddMul' α] (x y z : α) := x + y * z

Because AddMul is a 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, no additional declarations are necessary to use plusTimes1 with Nat:

37#eval plusTimes1 2 5 7 
37

However, plusTimes2 fails, because there is no AddMul' Nat instance—no instances whatsoever have yet been declared:

#eval failed to synthesize AddMul' ?m.22 Additional diagnostic information may be available using the `set_option diagnostics true` command.plusTimes2 2 5 7 
failed to synthesize
  AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Declaring an very general instance takes care of the problem for Nat and every other type:

instance [Add α] [Mul α] : AddMul' α where 37#eval plusTimes2 2 5 7 
37

3.7.2. Instance Declarations🔗

The syntax of instance declarations is almost identical to that of definitions. The only syntactic differences are that the keyword Lean.Parser.Command.declaration : commanddef is replaced by Lean.Parser.Command.declaration : commandinstance and the name is optional:

syntax

Most instances define each method using Lean.Parser.Command.declaration : commandwhere syntax:

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig where
        whereStructField*

However, type classes are inductive types, so instances can be constructed using any expression with an appropriate type:

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig :=
        termTermination hints are `termination_by` and `decreasing_by`, in that order.

Instances may also be defined by cases; however, this feature is rarely used outside of Decidable instances:

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig
        (| term => term)*Termination hints are `termination_by` and `decreasing_by`, in that order.

Instances defined with explicit terms often consist of either anonymous constructors (Lean.Parser.Term.anonymousCtor : termThe *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the expected type is an inductive type with a single constructor `c`. If more terms are given than `c` has parameters, the remaining arguments are turned into a new anonymous constructor application. For example, `⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`. ⟨...⟩) wrapping method implementations or of invocations of inferInstanceAs on definitionally equal types.

Elaboration of instances is almost identical to the elaboration of ordinary definitions, with the exception of the caveats documented below. If no name is provided, then one is created automatically. It is possible to refer to this generated name directly, but the algorithm used to generate the names has changed in the past and may change in the future. It's better to explicitly name instances that will be referred to directly. After elaboration, the new instance is registered as a candidate for instance search. Adding the attribute instance to a name can be used to mark any other defined name as a candidate.

Instance Name Generation

Following these declarations:

structure NatWrapper where val : Nat instance : BEq NatWrapper where beq | ⟨x⟩, ⟨y⟩ => x == y

the name instBEqNatWrapper refers to the new instance.

Variations in Instance Definitions

Given this structure type:

structure NatWrapper where val : Nat

all of the following ways of defining a BEq instance are equivalent:

instance : BEq NatWrapper where beq | ⟨x⟩, ⟨y⟩ => x == y instance : BEq NatWrapper := ⟨fun x y => x.val == y.val⟩ instance : BEq NatWrapper := ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩

Aside from introducing different names into the environment, the following are also equivalent:

@[instance] def instBeqNatWrapper : BEq NatWrapper where beq | ⟨x⟩, ⟨y⟩ => x == y instance : BEq NatWrapper := ⟨fun x y => x.val == y.val⟩ instance : BEq NatWrapper := ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩

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.

Instances are not recursive

Given this definition of NatTree:

inductive NatTree where | leaf | branch (left : NatTree) (val : Nat) (right : NatTree)

the following BEq instance fails:

instance : BEq NatTree where beq | .leaf, .leaf => true | .branch l1 v1 r1, .branch l2 v2 r2 => failed to synthesize BEq NatTree Additional diagnostic information may be available using the `set_option diagnostics true` command.l1 == l2 && v1 == v2 && failed to synthesize BEq NatTree Additional diagnostic information may be available using the `set_option diagnostics true` command.r1 == r2 | _, _ => false

with errors in both the left and right recursive calls that read:

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

Given a suitable recursive function, such as NatTree.beq:

def NatTree.beq : NatTree → NatTree → Bool | .leaf, .leaf => true | .branch l1 v1 r1, .branch l2 v2 r2 => l1 == l2 && v1 == v2 && r1 == r2 | _, _ => false

the instance can be created in a second step:

instance : BEq NatTree where beq := NatTree.beq

or, equivalently, using anonymous constructor syntax:

instance : BEq NatTree := ⟨NatTree.beq⟩

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.

Instances for nested types

In this definition of NatRoseTree, the type being defined occurs nested under another inductive type constructor (Array):

inductive NatRoseTree where | node (val : Nat) (children : Array NatRoseTree)

Checking the equality of rose trees requires checking equality of arrays. However, instances are not typically available for instance synthesis during their own definitions, so the following definition fails, even though NatRoseTree.beq is a recursive function and is in scope in its own definition.

def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool | .node val1 children1, .node val2 children2 => val1 == val2 && failed to synthesize BEq (Array NatRoseTree) Additional diagnostic information may be available using the `set_option diagnostics true` command.children1 == children2 
failed to synthesize
  BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

To solve this, a local BEq NatRoseTree instance may be let-bound:

partial def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool | .node val1 children1, .node val2 children2 => let _ : BEq NatRoseTree := ⟨NatRoseTree.beq⟩ val1 == val2 && children1 == children2

The use of array equality on the children finds the let-bound instance during instance synthesis.

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.

An instance for a sum class

Because DecidableEq α is an abbreviation for (a b : α) → Decidable (Eq a b), its arguments can be used directly, as in this example:

inductive ThreeChoices where | yes | no | maybe instance : DecidableEq ThreeChoices | .yes, .yes => .isTrue rfl | .no, .no => .isTrue rfl | .maybe, .maybe => .isTrue rfl | .yes, .maybe | .yes, .no | .maybe, .yes | .maybe, .no | .no, .yes | .no, .maybe => .isFalse nofun
A recursive instance for a sum class

The type StringList represents monomorphic lists of strings:

inductive StringList where | nil | cons (hd : String) (tl : StringList)

In the following attempt at defining a DecidableEq instance, instance synthesis invoked while elaborating the inner termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if fails because the instance is not available for instance synthesis in its own definition:

instance : DecidableEq StringList | .nil, .nil => .isTrue rfl | .cons h1 t1, .cons h2 t2 => if h : h1 = h2 then failed to synthesize Decidable (t1 = t2) Additional diagnostic information may be available using the `set_option diagnostics true` command.if h' : t1 = t2 then .isTrue (h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':t1 = t2⊢ StringList.cons h1 t1 = StringList.cons h2 t2 All goals completed! 🐙) else .isFalse (h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; h1:Stringt1:StringListh:h1 = h1h':¬t1 = t1⊢ False; All goals completed! 🐙) else .isFalse (h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; h1:Stringt1:StringListh:¬h1 = h1⊢ False; All goals completed! 🐙) | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun 
failed to synthesize
  Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

However, because it is an ordinary Lean function, it can recursively refer to its own explicitly-provided name:

instance instDecidableEqStringList : DecidableEq StringList | .nil, .nil => .isTrue rfl | .cons h1 t1, .cons h2 t2 => if h : h1 = h2 then if h' : application type mismatch @dite ?m.74 (instDecidableEqStringList t1 t2) argument instDecidableEqStringList t1 t2 has type Decidable (t1 = t2) : Type but is expected to have type Prop : TypeinstDecidableEqStringList t1 t2 then .isTrue (h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':sorry⊢ StringList.cons h1 t1 = StringList.cons h2 t2 h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':sorry⊢ t1 = t2) else .isFalse (h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬sorry⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬sorryhEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; h1:Stringt1:StringListh':¬sorryh:h1 = h1⊢ False; h1:Stringt1:StringListh':¬sorryh:h1 = h1⊢ False) else .isFalse (h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; h1:Stringt1:StringListh:¬h1 = h1⊢ False; All goals completed! 🐙) | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun

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.

syntax

Priorities may be numeric:

prio ::=
    num

If no priority is specified, the default priority that corresponds to 1000 is used:

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

Three named priorities are available when numeric values are too fine-grained, corresponding to 100, 500, and 10000 respectively. The prioMid : prioThe standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`. mid priority is lower than prioDefault : prioThe 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

Finally, priorities can be added and subtracted, so default + 2 is a valid priority, corresponding to 1002:

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.

syntax
attr ::= ...
    | default_instance prio?
Default Instances

A default instance of OfNat Nat is used to select Nat for natural number literals in the absence of other type information. It is declared in the Lean standard library with priority 100. Given this representation of even numbers, in which an even number is represented by half of it:

structure Even where half : Nat

the following instances allow numeric literals to be used for small Even values (a limit on the depth of type class instance search prevents them from being used for arbitrarily large literals):

instance ofNatEven0 : OfNat Even 0 where ofNat := ⟨0⟩ instance ofNatEvenPlusTwo [OfNat Even n] : OfNat Even (n + 2) where ofNat := ⟨(OfNat.ofNat n : Even).half + 1⟩ { half := 0 }#eval (0 : Even) { half := 17 }#eval (34 : Even) { half := 127 }#eval (254 : Even) 
{ half := 0 }

{ half := 17 }

{ half := 127 }

Specifying them as default instances with a priority greater than or equal to 100 causes them to be used instead of Nat:

attribute [default_instance 100] ofNatEven0 attribute [default_instance 100] ofNatEvenPlusTwo { half := 0 }#eval 0 { half := 17 }#eval 34 
{ half := 0 }

{ half := 17 }

Non-even numerals still use the OfNat Nat instance:

5#eval 5 
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.

syntax

Declares the definition to which it is applied to be an instance. If no priority is provided, then the default priority default is used.

attr ::= ...
    | instance prio?

3.7.3. Instance Synthesis🔗

Instance synthesis is a recursive search procedure that either finds an instance for a given type class or fails. In other words, given a type that is registered as a type class, instance synthesis attempts constructs a term with said type. It respects reducibility: semi-reducible or irreducible definitions are not unfolded, so instances for a definition are not automatically treated as instances for its unfolding unless it is reducible. There may be multiple possible instances for a given class; in this case, declared priorities and order of declaration are used as tiebreakers, in that order, with more recent instances taking precedence over earlier ones with the same priority.

This search procedure is efficient in the presence of diamonds and does not loop indefinitely when there are cycles. Diamonds occur when there is more than one route to a given goal, and cycles are situations when two instances each could be solved if the other were solved. Diamonds occur regularly in practice when encoding mathematical concepts using type classes, and Lean's coercion feature naturally leads to cycles, e.g. between finite sets and finite multisets.

Instance synthesis can be tested using the Lean.Parser.Command.synth : command#synth command.

syntax

The Lean.Parser.Command.synth : command#synth command attempts to synthesize an instance for the provided class. If it succeeds, then the resulting term is output.

command ::= ...
    | #synth term

Additionally, inferInstance and inferInstanceAs can be used to synthesize an instance in a position where the instance itself is needed.

🔗def
inferInstance.{u} {α : Sort u} [i : α] : α

inferInstance synthesizes a value of any target type by typeclass inference. This function has the same type signature as the identity function, but the square brackets on the [i : α] argument means that it will attempt to construct this argument by typeclass inference. (This will fail if α is not a class.) Example:

#check (inferInstance : Inhabited Nat) -- Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl
🔗def
inferInstanceAs.{u} (α : Sort u) [i : α] : α

inferInstanceAs α synthesizes a value of any target type by typeclass inference. This is just like inferInstance except that α is given explicitly instead of being inferred from the target type. It is especially useful when the target type is some α' which is definitionally equal to α, but the instance we are looking for is only registered for α (because typeclass search does not unfold most definitions, but definitional equality does.) Example:

#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat

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.

Local Instances

In this example, addPairs contains a locally-defined instance of Add NatPair:

structure NatPair where x : Nat y : Nat def addPairs (p1 p2 : NatPair) : NatPair := let _ : Add NatPair := ⟨fun ⟨x1, y1⟩ ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩⟩ p1 + p2

The local instance is used for the addition, having been found by instance synthesis.

Local Instances Have Priority

Here, addPairs contains a locally-defined instance of Add NatPair, even though there is a global instance:

structure NatPair where x : Nat y : Nat instance : Add NatPair where add | ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩ def addPairs (p1 p2 : NatPair) : NatPair := let _ : Add NatPair := ⟨fun _ _ => ⟨0, 0⟩⟩ p1 + p2

The local instance is selected instead of the global one:

{ x := 0, y := 0 }#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩ 
{ 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.

Implicit and Explicit Parameters to Instances

While instances typically take parameters either implicitly or instance-implicitly, explicit parameters may be filled out as if they were implicit during instance synthesis. In this example, aNonemptySumInstance is found by synthesis, applied explicitly to Nat, which is needed to make it type-correct.

instance aNonemptySumInstance (α : Type) {β : Type} [inst : Nonempty α] : Nonempty (α ⊕ β) := let ⟨x⟩ := inst ⟨.inl x⟩ set_option pp.explicit true in @aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)#synth Nonempty (Nat ⊕ Empty)

In the output, both the explicit argument Nat and the implicit argument Empty were found by unification with the search goal, while the Nonempty Nat instance was found via recursive instance synthesis.

@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.

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

Gadget for marking output parameters in type classes.

For example, the Membership class is defined as:

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

This means that whenever a typeclass goal of the form Membership ?α ?γ comes up, Lean will wait to solve it until ?γ is known, but then it will run typeclass inference, and take the first solution it finds, for any value of ?α, which thereby determines what ?α should be.

This expresses that in a term like a ∈ s, s might be a Set α or List α or some other type with a membership operation, and in each case the "member" type α is determined by looking at the container type.

Output Parameters and Stuck Search

This serialization framework provides a way to convert values to some underlying storage type:

class Serialize (input output : Type) where ser : input → output export Serialize (ser) instance : Serialize Nat String where ser n := toString n instance [Serialize α γ] [Serialize β γ] [Append γ] : Serialize (α × β) γ where ser | (x, y) => ser x ++ ser y

In this example, the output type is unknown.

example := typeclass instance problem is stuck, it is often due to metavariables Serialize (Nat × Nat) ?m.16ser (2, 3)

Instance synthesis can't select the Serialize Nat String instance, and thus the Append String instance, because that would require instantiating the output type as String, so the search gets stuck:

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

One way to fix the problem is to supply an expected type:

example : String := ser (2, 3)

The other is to make the output type into an output parameter:

class Serialize (input : Type) (output : outParam Type) where ser : input → output export Serialize (ser) instance : Serialize Nat String where ser n := toString n instance [Serialize α γ] [Serialize β γ] [Append γ] : Serialize (α × β) γ where ser | (x, y) => ser x ++ ser y

Now, instance synthesis is free to select the Serialize Nat String instance, which solves the unknown implicit output parameter of ser:

example := ser (2, 3)
Output Parameters with Pre-Existing Values

The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that has one fewer elements. There are two separate instances that can match an input type Option Bool, with different outputs:

class OneSmaller (α : Type) (β : outParam Type) where biggest : α shrink : (x : α) → x ≠ biggest → β instance : OneSmaller (Option α) α where biggest := none shrink | some x, _ => x instance : OneSmaller (Option Bool) (Option Unit) where biggest := some true shrink | none, _ => none | some false, _ => some () instance : OneSmaller Bool Unit where biggest := true shrink | false, _ => ()

Because instance synthesis selects the most recently defined instance, the following code is an error:

#check failed to synthesize OneSmaller (Option Bool) Bool Additional diagnostic information may be available using the `set_option diagnostics true` command.OneSmaller.shrink (β := Bool) (some false) sorry 
failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The OneSmaller (Option Bool) (Option Unit) instance was selected during instance synthesis, without regard to the supplied value of β.

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.

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

Gadget for marking semi output parameters in type classes.

Semi-output parameters influence the order in which arguments to type class instances are processed. Lean determines an order where all non-(semi-)output parameters to the instance argument have to be figured out before attempting to synthesize an argument (that is, they do not contain assignable metavariables created during TC synthesis). This rules out instances such as [Mul β] : Add α (because β could be anything). Marking a parameter as semi-output is a promise that instances of the type class will always fill in a value for that parameter.

For example, the Coe class is defined as:

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

This means that all Coe instances should provide a concrete value for α (i.e., not an assignable metavariable). An instance like Coe Nat Int or Coe α (Option α) is fine, but Coe α Nat is not since it does not provide a value for α.

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.

Semi-Output Parameters with Pre-Existing Values

The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that one fewer elements. It has two separate instances that can match an input type Option Bool, with different outputs:

class OneSmaller (α : Type) (β : semiOutParam Type) where biggest : α shrink : (x : α) → x ≠ biggest → β instance : OneSmaller (Option α) α where biggest := none shrink | some x, _ => x instance : OneSmaller (Option Bool) (Option Unit) where biggest := some true shrink | none, _ => none | some false, _ => some () instance : OneSmaller Bool Unit where biggest := true shrink | false, _ => ()

Because instance synthesis takes semi-output parameters into account when selecting instances, the OneSmaller (Option Bool) (Option Unit) instance is passed over due to the supplied value for β:

OneSmaller.shrink (some false) ⋯ : Bool#check OneSmaller.shrink (β := Bool) (some false) sorry 
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

🔗option
backward.synthInstance.canonInstances

Default value: true

use optimization that relies on 'morally canonical' instances during type class resolution

🔗option
synthInstance.maxHeartbeats

Default value: 20000

maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit

🔗option
synthInstance.maxSize

Default value: 128

maximum number of instances used to construct a solution in the type class instance synthesis procedure

3.7.4. Deriving Instances🔗

Lean can automatically generate instances for many classes, a process known as deriving instances. Instance deriving can be invoked either when defining a type or as a stand-alone command.

syntax

As part of a command that creates a new inductive type, a Lean.Parser.Command.declaration : commandderiving clause specifies a comma-separated list of class names for which instances should be generated:

optDeriving ::=
    (deriving ident,*)?
syntax

The stand-alone Lean.Parser.Command.deriving : commandderiving command specifies a number of class names and subject names. Each of the specified classes are derived for each of the specified subjects.

command ::= ...
    | deriving instance ident,* for ident,*
Deriving Multiple Classes

After specifying multiple classes to derive for multiple types, as in this code:

structure A where structure B where deriving instance BEq, Repr for A, B

all the instances exist for all the types, so all four Lean.Parser.Command.synth : command#synth commands succeed:

instBEqA#synth BEq A instBEqB#synth BEq B instReprA#synth Repr A instReprB#synth Repr B

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:

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

A DerivingHandler is called on the fully qualified names of all types it is running for as well as the syntax of a with argument, if present.

For example, deriving instance Foo with fooArgs for Bar, Baz invokes fooHandler #[`Bar, `Baz] `(fooArgs).

Deriving Handlers

Instances of the IsEnum class demonstrate that a type is a finite enumeration by providing a bijection between the type and a suitably-sized Fin:

class IsEnum (α : Type) where size : Nat toIdx : α → Fin size fromIdx : Fin size → α to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i from_to_id : ∀ (x : α), fromIdx (toIdx x) = x

For inductive types that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive. The instance for Bool is typical:

instance : IsEnum Bool where size := 2 toIdx | false => 0 | true => 1 fromIdx | 0 => false | 1 => true to_from_id | 0 => rfl | 1 => rfl from_to_id | false => rfl | true => rfl

The deriving handler programmatically constructs each pattern case, by analogy to the IsEnum Bool implementation:

open Lean Elab Parser Term Command def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do if h : declNames.size = 1 then let env ← getEnv if let some (.inductInfo ind) := env.find? declNames[0] then let mut tos : Array (TSyntax ``matchAlt) := #[] let mut froms := #[] let mut to_froms := #[] let mut from_tos := #[] let mut i := 0 for ctorName in ind.ctors do let c := mkIdent ctorName let n := Syntax.mkNumLit (toString i) tos := tos.push (← `(matchAltExpr| | $c => $n)) from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl)) froms := froms.push (← `(matchAltExpr| | $n => $c)) to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl)) i := i + 1 let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where size := $(quote ind.ctors.length) toIdx $tos:matchAlt* fromIdx $froms:matchAlt* to_from_id $to_froms:matchAlt* from_to_id $from_tos:matchAlt*) elabCommand cmd return true return false initialize registerDerivingHandler ``IsEnum deriveIsEnum

3.7.5. Basic Classes🔗

Many Lean type classes exist in order to allow built-in notations such as addition or array indexing to be overloaded.

3.7.5.1. Boolean Equality Tests

🔗type class
BEq.{u} (α : Type u) : Type u

BEq α is a typeclass for supplying a boolean-valued equality relation on α, notated as a == b. Unlike DecidableEq α (which uses a = b), this is Bool valued instead of Prop valued, and it also does not have any axioms like being reflexive or agreeing with =. It is mainly intended for programming applications. See LawfulBEq for a version that requires that == and = coincide.

Typically we prefer to put the "more variable" term on the left, and the "more constant" term on the right.

Instance Constructor

BEq.mk.{u} {α : Type u} (beq : α → α → Bool) : BEq α

Methods

beq:α → α → Bool

Boolean equality, notated as a == b.

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

A class for types that can be hashed into a UInt64.

Instance Constructor

Hashable.mk.{u} {α : Sort u} (hash : α → UInt64) : Hashable α

Methods

hash:α → UInt64

Hashes the value a : α into a UInt64.

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

LawfulBEq α is a typeclass which asserts that the BEq α implementation (which supplies the a == b notation) coincides with logical equality a = b. In other words, a == b implies a = b, and a == a is true.

Instance Constructor

LawfulBEq.mk.{u} {α : Type u} [BEq α] (eq_of_beq : ∀ {a b : α}, (a == b) = true → a = b) (rfl : ∀ {a : α}, (a == a) = true) : LawfulBEq α

Methods

eq_of_beq:∀ {a b : α}, (a == b) = true → a = b

If a == b evaluates to true, then a and b are equal in the logic.

rfl:∀ {a : α}, (a == a) = true

== is reflexive, that is, (a == a) = true.

3.7.5.2. Ordering

🔗type class
Ord.{u} (α : Type u) : Type u

Ord α provides a computable total order on α, in terms of the compare : α → α → Ordering function.

Typically instances will be transitive, reflexive, and antisymmetric, but this is not enforced by the typeclass.

There is a derive handler, so appending deriving Ord to an inductive type or structure will attempt to create an Ord instance.

Instance Constructor

Ord.mk.{u} {α : Type u} (compare : α → α → Ordering) : Ord α

Methods

compare:α → α → Ordering

Compare two elements in α using the comparator contained in an [Ord α] instance.

🔗type class
LT.{u} (α : Type u) : Type u

LT α is the typeclass which supports the notation x < y where x y : α.

Instance Constructor

LT.mk.{u} {α : Type u} (lt : α → α → Prop) : LT α

Methods

lt:α → α → Prop

The less-than relation: x < y

🔗type class
LE.{u} (α : Type u) : Type u

LE α is the typeclass which supports the notation x ≤ y where x y : α.

Instance Constructor

LE.mk.{u} {α : Type u} (le : α → α → Prop) : LE α

Methods

le:α → α → Prop

The less-equal relation: x ≤ y

3.7.5.3. Decidability

🔗inductive type
Decidable (p : Prop) : Type

Decidable p is a data-carrying class that supplies a proof that p is either true or false. It is equivalent to Bool (and in fact it has the same code generation as Bool) together with a proof that the Bool is true iff p is.

Decidable instances are used to infer "computation strategies" for propositions, so that you can have the convenience of writing propositions inside if statements and executing them (which actually executes the inferred decidability instance instead of the proposition, which has no code).

If a proposition p is Decidable, then (by decide : p) will prove it by evaluating the decidability instance to isTrue h and returning h.

Because Decidable carries data, when writing @[simp] lemmas which include a Decidable instance on the LHS, it is best to use {_ : Decidable p} rather than [Decidable p] so that non-canonical instances can be found via unification rather than typeclass search.

Constructors

  • isFalse {p : Prop} (h : ¬p) : _root_.Decidable p

    Prove that p is decidable by supplying a proof of ¬p

  • isTrue {p : Prop} (h : p) : _root_.Decidable p

    Prove that p is decidable by supplying a proof of p

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

A decidable relation. See Decidable.

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

Asserts that α has decidable equality, that is, a = b is decidable for all a b : α. See Decidable.

3.7.5.4. Inhabited Types

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

Inhabited α is a typeclass that says that α has a designated element, called (default : α). This is sometimes referred to as a "pointed type".

This class is used by functions that need to return a value of the type when called "out of domain". For example, Array.get! arr i : α returns a value of type α when arr : Array α, but if i is not in range of the array, it reports a panic message, but this does not halt the program, so it must still return a value of type α (and in fact this is required for logical consistency), so in this case it returns default.

Instance Constructor

Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α

Methods

default:α

default is a function that produces a "default" element of any Inhabited type. This element does not have any particular specified properties, but it is often an all-zeroes value.

🔗inductive predicate
Nonempty.{u} (α : Sort u) : Prop

Nonempty α is a typeclass that says that α is not an empty type, that is, there exists an element in the type. It differs from Inhabited α in that Nonempty α is a Prop, which means that it does not actually carry an element of α, only a proof that there exists such an element. Given Nonempty α, you can construct an element of α nonconstructively using Classical.choice.

Constructors

  • intro.{u} {α : Sort u} (val : α) : _root_.Nonempty α

    If val : α, then α is nonempty.

3.7.5.5. Visible Representations

Planned Content

  • How to write a correct Repr instance

  • ReprAtom

  • Useful helpers, like Repr.addAppParen and reprArg

  • When to use Repr vs ToString

Tracked at issue #135

🔗type class
Repr.{u} (α : Type u) : Type u

A typeclass that specifies the standard way of turning values of some type into Format.

When rendered this Format should be as close as possible to something that can be parsed as the input value.

Instance Constructor

Repr.mk.{u} {α : Type u} (reprPrec : α → Nat → Lean.Format) : Repr α

Methods

reprPrec:α → Nat → Lean.Format

Turn a value of type α into Format at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.

🔗type class
ToString.{u} (α : Type u) : Type u

Instance Constructor

ToString.mk.{u} {α : Type u} (toString : α → String) : ToString α

Methods

toString:α → String

3.7.5.6. Arithmetic and Bitwise Operators

🔗type class
Zero.{u} (α : Type u) : Type u

A type with a zero element.

Instance Constructor

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

Methods

zero:α

The zero element of the type.

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

A type-class version of n ≠ 0.

Instance Constructor

NeZero.mk.{u_1} {R : Type u_1} [Zero R] {n : R} (out : n ≠ 0) : NeZero n

Methods

out:n ≠ 0

The proposition that n is not zero.

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

The notation typeclass for heterogeneous addition. This enables the notation a + b : γ where a : α, b : β.

Instance Constructor

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

Methods

hAdd:α → β → γ

a + b computes the sum of a and b. The meaning of this notation is type-dependent.

🔗type class
Add.{u} (α : Type u) : Type u

The homogeneous version of HAdd: a + b : α where a b : α.

Instance Constructor

Add.mk.{u} {α : Type u} (add : α → α → α) : Add α

Methods

add:α → α → α

a + b computes the sum of a and b. See HAdd.

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

The notation typeclass for heterogeneous subtraction. This enables the notation a - b : γ where a : α, b : β.

Instance Constructor

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

Methods

hSub:α → β → γ

a - b computes the difference of a and b. The meaning of this notation is type-dependent.

  • For natural numbers, this operator saturates at 0: a - b = 0 when a ≤ b.

🔗type class
Sub.{u} (α : Type u) : Type u

The homogeneous version of HSub: a - b : α where a b : α.

Instance Constructor

Sub.mk.{u} {α : Type u} (sub : α → α → α) : Sub α

Methods

sub:α → α → α

a - b computes the difference of a and b. See HSub.

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

The notation typeclass for heterogeneous multiplication. This enables the notation a * b : γ where a : α, b : β.

Instance Constructor

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

Methods

hMul:α → β → γ

a * b computes the product of a and b. The meaning of this notation is type-dependent.

🔗type class
Mul.{u} (α : Type u) : Type u

The homogeneous version of HMul: a * b : α where a b : α.

Instance Constructor

Mul.mk.{u} {α : Type u} (mul : α → α → α) : Mul α

Methods

mul:α → α → α

a * b computes the product of a and b. See HMul.

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

The notation typeclass for heterogeneous division. This enables the notation a / b : γ where a : α, b : β.

Instance Constructor

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

Methods

hDiv:α → β → γ

a / b computes the result of dividing a by b. The meaning of this notation is type-dependent.

  • For most types like Nat, Int, Rat, Real, a / 0 is defined to be 0.

  • For Nat, a / b rounds downwards.

  • For Int, a / b rounds downwards if b is positive or upwards if b is negative. It is implemented as Int.ediv, the unique function satisfying a % b + b * (a / b) = a and 0 ≤ a % b < natAbs b for b ≠ 0. Other rounding conventions are available using the functions Int.fdiv (floor rounding) and Int.div (truncation rounding).

  • For Float, a / 0 follows the IEEE 754 semantics for division, usually resulting in inf or nan.

🔗type class
Div.{u} (α : Type u) : Type u

The homogeneous version of HDiv: a / b : α where a b : α.

Instance Constructor

Div.mk.{u} {α : Type u} (div : α → α → α) : Div α

Methods

div:α → α → α

a / b computes the result of dividing a by b. See HDiv.

🔗type class
Dvd.{u_1} (α : Type u_1) : Type u_1

Notation typeclass for the ∣ operation (typed as \|), which represents divisibility.

Instance Constructor

Dvd.mk.{u_1} {α : Type u_1} (dvd : α → α → Prop) : Dvd α

Methods

dvd:α → α → Prop

Divisibility. a ∣ b (typed as \|) means that there is some c such that b = a * c.

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

The notation typeclass for heterogeneous modulo / remainder. This enables the notation a % b : γ where a : α, b : β.

Instance Constructor

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

Methods

hMod:α → β → γ

a % b computes the remainder upon dividing a by b. The meaning of this notation is type-dependent.

  • For Nat and Int it satisfies a % b + b * (a / b) = a, and a % 0 is defined to be a.

🔗type class
Mod.{u} (α : Type u) : Type u

The homogeneous version of HMod: a % b : α where a b : α.

Instance Constructor

Mod.mk.{u} {α : Type u} (mod : α → α → α) : Mod α

Methods

mod:α → α → α

a % b computes the remainder upon dividing a by b. See HMod.

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

The notation typeclass for heterogeneous exponentiation. This enables the notation a ^ b : γ where a : α, b : β.

Instance Constructor

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

Methods

hPow:α → β → γ

a ^ b computes a to the power of b. The meaning of this notation is type-dependent.

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

The homogeneous version of HPow: a ^ b : α where a : α, b : β. (The right argument is not the same as the left since we often want this even in the homogeneous case.)

Types can choose to subscribe to particular defaulting behavior by providing an instance to either NatPow or HomogeneousPow:

  • NatPow is for types whose exponents is preferentially a Nat.

  • HomogeneousPow is for types whose base and exponent are preferentially the same.

Instance Constructor

Pow.mk.{u, v} {α : Type u} {β : Type v} (pow : α → β → α) : Pow α β

Methods

pow:α → β → α

a ^ b computes a to the power of b. See HPow.

🔗type class
NatPow.{u} (α : Type u) : Type u

The homogeneous version of Pow where the exponent is a Nat. The purpose of this class is that it provides a default Pow instance, which can be used to specialize the exponent to Nat during elaboration.

For example, if x ^ 2 should preferentially elaborate with 2 : Nat then x's type should provide an instance for this class.

Instance Constructor

NatPow.mk.{u} {α : Type u} (pow : α → Nat → α) : NatPow α

Methods

pow:α → Nat → α

a ^ n computes a to the power of n where n : Nat. See Pow.

🔗type class
HomogeneousPow.{u} (α : Type u) : Type u

The completely homogeneous version of Pow where the exponent has the same type as the base. The purpose of this class is that it provides a default Pow instance, which can be used to specialize the exponent to have the same type as the base's type during elaboration. This is to say, a type should provide an instance for this class in case x ^ y should be elaborated with both x and y having the same type.

For example, the Float type provides an instance of this class, which causes expressions such as (2.2 ^ 2.2 : Float) to elaborate.

Instance Constructor

HomogeneousPow.mk.{u} {α : Type u} (pow : α → α → α) : HomogeneousPow α

Methods

pow:α → α → α

a ^ b computes a to the power of b where a and b both have the same type.

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

The typeclass behind the notation a <<< b : γ where a : α, b : β.

Instance Constructor

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

Methods

hShiftLeft:α → β → γ

a <<< b computes a shifted to the left by b places. The meaning of this notation is type-dependent.

  • On Nat, this is equivalent to a * 2 ^ b.

  • On UInt8 and other fixed width unsigned types, this is the same but truncated to the bit width.

🔗type class
ShiftLeft.{u} (α : Type u) : Type u

The homogeneous version of HShiftLeft: a <<< b : α where a b : α.

Instance Constructor

ShiftLeft.mk.{u} {α : Type u} (shiftLeft : α → α → α) : ShiftLeft α

Methods

shiftLeft:α → α → α

The implementation of a <<< b : α. See HShiftLeft.

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

The typeclass behind the notation a >>> b : γ where a : α, b : β.

Instance Constructor

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

Methods

hShiftRight:α → β → γ

a >>> b computes a shifted to the right by b places. The meaning of this notation is type-dependent.

  • On Nat and fixed width unsigned types like UInt8, this is equivalent to a / 2 ^ b.

🔗type class
ShiftRight.{u} (α : Type u) : Type u

The homogeneous version of HShiftRight: a >>> b : α where a b : α.

Instance Constructor

ShiftRight.mk.{u} {α : Type u} (shiftRight : α → α → α) : ShiftRight α

Methods

shiftRight:α → α → α

The implementation of a >>> b : α. See HShiftRight.

🔗type class
Neg.{u} (α : Type u) : Type u

The notation typeclass for negation. This enables the notation -a : α where a : α.

Instance Constructor

Neg.mk.{u} {α : Type u} (neg : α → α) : Neg α

Methods

neg:α → α

-a computes the negative or opposite of a. The meaning of this notation is type-dependent.

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

The typeclass behind the notation a &&& b : γ where a : α, b : β.

Instance Constructor

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

Methods

hAnd:α → β → γ

a &&& b computes the bitwise AND of a and b. The meaning of this notation is type-dependent.

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

The typeclass behind the notation a ||| b : γ where a : α, b : β.

Instance Constructor

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

Methods

hOr:α → β → γ

a ||| b computes the bitwise OR of a and b. The meaning of this notation is type-dependent.

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

The typeclass behind the notation a ^^^ b : γ where a : α, b : β.

Instance Constructor

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

Methods

hXor:α → β → γ

a ^^^ b computes the bitwise XOR of a and b. The meaning of this notation is type-dependent.

3.7.5.7. Append

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

The notation typeclass for heterogeneous append. This enables the notation a ++ b : γ where a : α, b : β.

Instance Constructor

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

Methods

hAppend:α → β → γ

a ++ b is the result of concatenation of a and b, usually read "append". The meaning of this notation is type-dependent.

🔗type class
Append.{u} (α : Type u) : Type u

The homogeneous version of HAppend: a ++ b : α where a b : α.

Instance Constructor

Append.mk.{u} {α : Type u} (append : α → α → α) : Append α

Methods

append:α → α → α

a ++ b is the result of concatenation of a and b. See HAppend.

3.7.5.8. Data Lookups

🔗type class
GetElem.{u, v, w} (coll : Type u) (idx : Type v)
    (elem : outParam (Type w))
    (valid : outParam (coll → idx → Prop))
    : Type (max (max u v) w)

The classes GetElem and GetElem? implement lookup notation, specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.

Both classes are indexed by types coll, idx, and elem which are the collection, the index, and the element types. A single collection may support lookups with multiple index types. The relation valid determines when the index is guaranteed to be valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an array xs and a natural number i, xs[i] will return an α when valid xs i holds, which is true when i is less than the size of the array. Array additionally supports indexing with USize instead of Nat. In either case, because the bounds are checked at compile time, no runtime check is required.

Given xs[i] with xs : coll and i : idx, Lean looks for an instance of GetElem coll idx elem valid and uses this to infer the type of the return value elem and side condition valid required to ensure xs[i] yields a valid value of type elem. The tactic get_elem_tactic is invoked to prove validity automatically. The xs[i]'p notation uses the proof p to satisfy the validity condition. If the proof p is long, it is often easier to place the proof in the context using have, because get_elem_tactic tries assumption.

The proof side-condition valid xs i is automatically dispatched by the get_elem_tactic tactic; this tactic can be extended by adding more clauses to get_elem_tactic_trivial using macro_rules.

xs[i]? and xs[i]! do not impose a proof obligation; the former returns an Option elem, with none signalling that the value isn't present, and the latter returns elem but panics if the value isn't there, returning default : elem based on the Inhabited elem instance. These are provided by the GetElem? class, for which there is a default instance generated from a GetElem class as long as valid xs i is always decidable.

Important instances include:

  • arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no runtime bounds check and a proof side goal i < arr.size.

  • l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.

Instance Constructor

GetElem.mk.{u, v, w} {coll : Type u} {idx : Type v} {elem : outParam (Type w)} {valid : outParam (coll → idx → Prop)} (getElem : (xs : coll) → (i : idx) → valid xs i → elem) : GetElem coll idx elem valid

Methods

getElem:(xs : coll) → (i : idx) → valid xs i → elem

The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

🔗type class
GetElem?.{u, v, w} (coll : Type u)
    (idx : Type v) (elem : outParam (Type w))
    (valid : outParam (coll → idx → Prop))
    : Type (max (max u v) w)

The classes GetElem and GetElem? implement lookup notation, specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.

Both classes are indexed by types coll, idx, and elem which are the collection, the index, and the element types. A single collection may support lookups with multiple index types. The relation valid determines when the index is guaranteed to be valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an array xs and a natural number i, xs[i] will return an α when valid xs i holds, which is true when i is less than the size of the array. Array additionally supports indexing with USize instead of Nat. In either case, because the bounds are checked at compile time, no runtime check is required.

Given xs[i] with xs : coll and i : idx, Lean looks for an instance of GetElem coll idx elem valid and uses this to infer the type of the return value elem and side condition valid required to ensure xs[i] yields a valid value of type elem. The tactic get_elem_tactic is invoked to prove validity automatically. The xs[i]'p notation uses the proof p to satisfy the validity condition. If the proof p is long, it is often easier to place the proof in the context using have, because get_elem_tactic tries assumption.

The proof side-condition valid xs i is automatically dispatched by the get_elem_tactic tactic; this tactic can be extended by adding more clauses to get_elem_tactic_trivial using macro_rules.

xs[i]? and xs[i]! do not impose a proof obligation; the former returns an Option elem, with none signalling that the value isn't present, and the latter returns elem but panics if the value isn't there, returning default : elem based on the Inhabited elem instance. These are provided by the GetElem? class, for which there is a default instance generated from a GetElem class as long as valid xs i is always decidable.

Important instances include:

  • arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no runtime bounds check and a proof side goal i < arr.size.

  • l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.

Instance Constructor

GetElem?.mk.{u, v, w} {coll : Type u} {idx : Type v} {elem : outParam (Type w)} {valid : outParam (coll → idx → Prop)} [toGetElem : GetElem coll idx elem valid] (getElem? : coll → idx → Option elem) (getElem! : [inst : Inhabited elem] → coll → idx → elem) : GetElem? coll idx elem valid

Methods

toGetElem:GetElem coll idx elem valid
getElem?:coll → idx → Option elem

The syntax arr[i]? gets the i'th element of the collection arr, if it is present (and wraps it in some), and otherwise returns none.

getElem!:[inst : Inhabited elem] → coll → idx → elem

The syntax arr[i]! gets the i'th element of the collection arr, if it is present, and otherwise panics at runtime and returns the default term from Inhabited elem.

🔗type class
LawfulGetElem.{u, v, w} (cont : Type u)
  (idx : Type v) (elem : outParam (Type w))
  (dom : outParam (cont → idx → Prop))
  [ge : GetElem? cont idx elem dom] : Prop

Instance Constructor

LawfulGetElem.mk.{u, v, w} {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)} [ge : GetElem? cont idx elem dom] (getElem?_def : ∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i thenA some c[i] else none := by intros try simp only [getElem?] <;> congr) (getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx), c[i]! = match c[i]? withA | some e => e | none => default := by intros simp only [getElem!, getElem?, outOfBounds_eq_default]) : LawfulGetElem cont idx elem dom

Methods

getElem!_def:∀ [inst : Inhabited elem] (c : cont) (i : idx), c[i]! = match c[i]? withA | some e => e | none => default
getElem?_def:∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i thenA some c[i] else none