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

Types that can be hashed into a UInt64.

Instance Constructor

Hashable.mk.{u}

Methods

hash : α → UInt64

An opaque hash mixing operation, used to implement hashing for products.

A Boolean equality test coincides with propositional equality.

In other words:

• a == b implies a = b.

• a == a is true.

Instance Constructor

LawfulBEq.mk.{u}

Methods

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

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

The BEq α and Hashable α instances on α are compatible. This means that that a == b implies hash a = hash b.

This is automatic if the BEq instance is lawful.

Instance Constructor

LawfulHashable.mk.{u}

Methods

hash_eq : ∀ (a b : α), (a == b) = true → hash a = hash b

A lawful hash function respects its Boolean equality test.

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

Compares two values by comparing the results of applying a function.

In particular, x is compared to y by comparing f x and f y.

Examples:

• compareOn (·.length) "apple" "banana" = .lt

• compareOn (· % 3) 5 6 = .gt

• compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq

Inverts the order of an Ord instance.

The result is an Ord α instance that returns Ordering.lt when ord would return Ordering.gt and that returns Ordering.gt when ord would return Ordering.lt.

The result of a comparison according to a total order.

The relationship between the compared items may be:

• Ordering.lt: less than

• Ordering.eq: equal

• Ordering.gt: greater than

Constructors

lt : Ordering

eq : Ordering

gt : Ordering

Swaps less-than and greater-than ordering results.

Examples:

• Ordering.lt.swap = Ordering.gt

• Ordering.eq.swap = Ordering.eq

• Ordering.gt.swap = Ordering.lt

If a and b are Ordering, then a.then b returns a unless it is .eq, in which case it returns b. Additionally, it has “short-circuiting” behavior similar to boolean &&: if a is not .eq then the expression for b is not evaluated.

This is a useful primitive for constructing lexicographic comparator functions. The deriving Ord syntax on a structure uses the Ord instance to compare each field in order, combining the results equivalently to Ordering.then.

Use compareLex to lexicographically combine two comparison functions.

Examples:

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩

#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩

Checks whether the ordering is lt.

Checks whether the ordering is lt or eq.

Checks whether the ordering is eq.

Checks whether the ordering is not eq.

Checks whether the ordering is gt or eq.

Checks whether the ordering is gt.

Uses decidable less-than and equality relations to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x = y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndBEq uses BEq instead of DecidableEq.

Uses a decidable less-than relation and Boolean equality to find an Ordering.

In particular, if x < y then the result is Ordering.lt. If x == y then the result is Ordering.eq. Otherwise, it is Ordering.gt.

compareOfLessAndEq uses DecidableEq instead of BEq.

Compares a and b lexicographically by cmp₁ and cmp₂.

a and b are first compared by cmp₁. If this returns Ordering.eq, a and b are compared by cmp₂ to break the tie.

To lexicographically combine two Orderings, use Ordering.then.

The less-than operator is overloaded in the LT class:

term ::= ...
    | The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.term < term

The less-than-or-equal-to operator is overloaded in the LE class:

term ::= ...
    | The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.term ≤ term

The greater-than and greater-than-or-equal-to operators are the reverse of the less-than and less-than-or-equal-to operators, and cannot be independently overloaded:

term ::= ...
    | `a > b` is an abbreviation for `b < a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>` in identifiers is `gt`.term > term

term ::= ...
    | `a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.term ≥ term

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

Instance Constructor

LT.mk.{u}

Methods

lt : α → α → Prop

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

Instance Constructor

LE.mk.{u}

Methods

le : α → α → Prop

Constructs an LT instance from an Ord instance that asserts that the result of compare is Ordering.lt.

Constructs an LT instance from an Ord instance that asserts that the result of compare satisfies Ordering.isLE.

Constructs a BEq instance from an Ord instance.

Constructs an LE instance from an Ord instance.

Constructs an LT instance from an Ord instance.

An overloaded operation to find the lesser of two values of type α.

Instance Constructor

Min.mk.{u}

Methods

min : α → α → α

An overloaded operation to find the greater of two values of type α.

Instance Constructor

Max.mk.{u}

Methods

max : α → α → α

Constructs a Min instance from a decidable ≤ operation.

Constructs a Max instance from a decidable ≤ operation.

Either a proof that p is true or a proof that p is false. This is equivalent to a Bool paired with a proof that the Bool is true if and only if p is true.

Decidable instances are primarily used via if-expressions and the tactic decide. In conditional expressions, the Decidable instance for the proposition is used to select a branch. At run time, this case distinction code is identical to that which would be generated for a Bool-based conditional. In proofs, the tactic decide synthesizes an instance of Decidable p, attempts to reduce it to isTrue h, and then succeeds with the proof h if it can.

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 instance synthesis.

Constructors

isFalse {p : Prop} (h : ¬p) : Decidable p

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

A decidable predicate.

A predicate is decidable if the corresponding proposition is Decidable for each possible argument.

A decidable relation.

A relation is decidable if the corresponding proposition is Decidable for all possible arguments.

Propositional equality is Decidable for all elements of a type.

In other words, an instance of DecidableEq α is a means of deciding the proposition a = b is for all a b : α.

Abbreviation for DecidableRel (· < · : α → α → Prop).

Abbreviation for DecidableRel (· ≤ · : α → α → Prop).

Converts a decidable proposition into a Bool.

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

Construct a q if some proposition p is decidable, and both the truth and falsity of p are sufficient to construct a q.

This is a synonym for dite, the dependent if-then-else operator.

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

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 α

A subsingleton is a type with at most one element. It is either empty or has a unique element.

All propositions are subsingletons because of proof irrelevance: false propositions are empty, and all proofs of a true proposition are equal to one another. Some non-propositional types are also subsingletons.

Instance Constructor

Subsingleton.intro.{u}

Methods

allEq : ∀ (a b : α), a = b

If a type is a subsingleton, then all of its elements are equal.

If two types are equal and one of them is a subsingleton, then all of their elements are heterogeneously equal.

A type with a zero element.

Instance Constructor

Zero.mk.{u}

Methods

zero : α

A type-class version of n ≠ 0.

Instance Constructor

NeZero.mk.{u_1}

Methods

out : n ≠ 0

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

Instance Constructor

HAdd.mk.{u, v, w}

Methods

hAdd : α → β → γ

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

Instance Constructor

Add.mk.{u}

Methods

add : α → α → α

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

Instance Constructor

HSub.mk.{u, v, w}

Methods

hSub : α → β → γ

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

Instance Constructor

Sub.mk.{u}

Methods

sub : α → α → α

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

Instance Constructor

HMul.mk.{u, v, w}

Methods

hMul : α → β → γ

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

Instance Constructor

Mul.mk.{u}

Methods

mul : α → α → α

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

Instance Constructor

HDiv.mk.{u, v, w}

Methods

hDiv : α → β → γ

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

Instance Constructor

Div.mk.{u}

Methods

div : α → α → α

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

Instance Constructor

Dvd.mk.{u_1}

Methods

dvd : α → α → Prop

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 : α → β → γ

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

Instance Constructor

Mod.mk.{u}

Methods

mod : α → α → α

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

Instance Constructor

HPow.mk.{u, v, w}

Methods

hPow : α → β → γ

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 : α → β → α

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 → α

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 : α → α → α

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

Instance Constructor

HShiftLeft.mk.{u, v, w}

Methods

hShiftLeft : α → β → γ

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

Instance Constructor

ShiftLeft.mk.{u}

Methods

shiftLeft : α → α → α

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

Instance Constructor

HShiftRight.mk.{u, v, w}

Methods

hShiftRight : α → β → γ

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

Instance Constructor

ShiftRight.mk.{u}

Methods

shiftRight : α → α → α

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

Instance Constructor

Neg.mk.{u}

Methods

neg : α → α

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

Instance Constructor

HAnd.mk.{u, v, w}

Methods

hAnd : α → β → γ

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

Instance Constructor

HOr.mk.{u, v, w}

Methods

hOr : α → β → γ

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

Instance Constructor

HXor.mk.{u, v, w}

Methods

hXor : α → β → γ

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

Instance Constructor

HAppend.mk.{u, v, w}

Methods

hAppend : α → β → γ

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

Instance Constructor

Append.mk.{u}

Methods

append : α → α → α

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

getElem? : coll → idx → Option elem

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

Lawful GetElem? instances (which extend GetElem) are those for which the potentially-failing GetElem?.getElem? and GetElem?.getElem! operators succeed when the validity predicate is satisfied, and fail when it is not.

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 then some c[i] else none

getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx),
  c[i]! =
    match c[i]? with
    | some e => e
    | none => default