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}

Methods

beq	:	α → α → Bool
		Boolean equality, notated as a == b.

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

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

Instance Constructor

Hashable.mk.{u}

Methods

hash	:	α → UInt64
		Hashes the value a : α into a UInt64.

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}

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.

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}

Methods

compare	:	α → α → Ordering
		Compare two elements in α using the comparator contained in an [Ord α] instance.

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

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

Instance Constructor

LT.mk.{u}

Methods

lt	:	α → α → Prop
		The less-than relation: x < y

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

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

Instance Constructor

LE.mk.{u}

Methods

le	:	α → α → Prop
		The less-equal relation: x ≤ y

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) : Decidable p

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

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

  Prove that p is decidable by supplying a proof of p

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

A decidable relation. See Decidable.

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.

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

Convert a decidable proposition into a boolean value.

If p : Prop is decidable, then decide p : Bool is the boolean value which is true if p is true and false if p is false.

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

Synonym for dite (dependent if-then-else). We can construct an element q (of any sort, not just a proposition) by cases on whether p is true or false, provided p is decidable.

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}

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.

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 : α) : Nonempty α

  If val : α, then α is nonempty.

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}

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.

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

Instance Constructor

ToString.mk.{u}

Methods

toString

:

α → String

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

A type with a zero element.

Instance Constructor

Zero.mk.{u}

Methods

zero	:	α
		The zero element of the type.

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}

Methods

out	:	n ≠ 0
		The proposition that n is not zero.

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}

Methods

hAdd	:	α → β → γ
		a + b computes the sum of a and b. The meaning of this notation is type-dependent.

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

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

Instance Constructor

Add.mk.{u}

Methods

add	:	α → α → α
		a + b computes the sum of a and b. See HAdd.

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}

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.

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

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

Instance Constructor

Sub.mk.{u}

Methods

sub	:	α → α → α
		a - b computes the difference of a and b. See HSub.

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}

Methods

hMul	:	α → β → γ
		a * b computes the product of a and b. The meaning of this notation is type-dependent.

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

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

Instance Constructor

Mul.mk.{u}

Methods

mul	:	α → α → α
		a * b computes the product of a and b. See HMul.

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}

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.

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

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

Instance Constructor

Div.mk.{u}

Methods

div	:	α → α → α
		a / b computes the result of dividing a by b. See HDiv.

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}

Methods

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

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}

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.

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

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

Instance Constructor

Mod.mk.{u}

Methods

mod	:	α → α → α
		a % b computes the remainder upon dividing a by b. See HMod.

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}

Methods

hPow	:	α → β → γ
		a ^ b computes a to the power of b. The meaning of this notation is type-dependent.

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}

Methods

pow	:	α → β → α
		a ^ b computes a to the power of b. See HPow.

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}

Methods

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

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}

Methods

pow	:	α → α → α
		a ^ b computes a to the power of b where a and b both have the same type.

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}

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.

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

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

Instance Constructor

ShiftLeft.mk.{u}

Methods

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

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}

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.

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

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

Instance Constructor

ShiftRight.mk.{u}

Methods

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

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

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

Instance Constructor

Neg.mk.{u}

Methods

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

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}

Methods

hAnd	:	α → β → γ
		a &&& b computes the bitwise AND of a and b. The meaning of this notation is type-dependent.

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}

Methods

hOr	:	α → β → γ
		a ||| b computes the bitwise OR of a and b. The meaning of this notation is type-dependent.

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}

Methods

hXor	:	α → β → γ
		a ^^^ b computes the bitwise XOR of a and b. The meaning of this notation is type-dependent.

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}

Methods

hAppend	:	α → β → γ
		a ++ b is the result of concatenation of a and b, usually read "append". The meaning of this notation is type-dependent.

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

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

Instance Constructor

Append.mk.{u}

Methods

append	:	α → α → α
		a ++ b is the result of concatenation of a and b. See HAppend.

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}

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.

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}

Extends

• GetElem coll idx elem valid

Methods

getElem	:	(xs : coll) → (i : idx) → valid xs i → elem
		Inherited from GetElem
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.

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}

Methods

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