# Init.Prelude #

This is the first file in the Lean import hierarchy. It is responsible for setting up basic definitions, most of which Lean already has "built in knowledge" about, so it is important that they be set up in exactly this way. (For example, Lean will use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler.)

source
@[inline]
def id {α : Sort u} (a : α) :
α

The identity function. `id` takes an implicit argument `α : Sort u` (a type in any universe), and an argument `a : α`, and returns `a`.

Although this may look like a useless function, one application of the identity function is to explicitly put a type on an expression. If `e` has type `T`, and `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and Lean knows that this expression has type `T'` rather than `T`. This can make a difference for typeclass inference, since `T` and `T'` may have different typeclass instances on them. `show T' from e` is sugar for an `@id T' e` expression.

Equations

- id a = a

Instances For

source
@[inline]
def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) :
α → δ

Function composition, usually written with the infix operator `∘`. A new function is created from two existing functions, where one function's output is used as input to the other.

Examples:

- `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
- `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`

Conventions for notations in identifiers:

- The recommended spelling of `∘` in identifiers is `comp`.

Equations

- (f ∘ g) x = f (g x)

Instances For

source
@[inline]
def Function.const {α : Sort u} (β : Sort v) (a : α) :
β → α

The constant function that ignores its argument.

If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all arguments `b : β`, `Function.const β a b = a`.

Examples:

- `Function.const Bool 10 true = 10`
- `Function.const Bool 10 false = 10`
- `Function.const String 10 "any string" = 10`

Equations

- Function.const β a x✝ = a

Instances For

source
def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) :
β v

`letFun v (fun x => b)` is a function version of `have x := v; b`. This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`. This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.

This used to be the way `have`/`let_fun` syntax was encoded, and there used to be special support for `letFun` in WHNF and `simp`.

Equations

- letFun v f = f v

Instances For

source
@[reducible, inline]
abbrev inferInstance {α : 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

Equations

- inferInstance = i

Instances For

source
@[reducible, inline]
abbrev inferInstanceAs (α : 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

Equations

- inferInstanceAs α = i

Instances For

source
inductive PUnit :
Sort u

The canonical universe-polymorphic type with just one element.

It should be used in contexts that require a type to be universe polymorphic, thus disallowing `Unit`.

- unit : PUnit

  The only element of the universe-polymorphic unit type.

Instances For

source
@[reducible, inline]
abbrev Unit :
Type

The canonical type with one element. This element is written `()`.

`Unit` has a number of uses:

- It can be used to model control flow that returns from a function call without providing other information.
- Monadic actions that return `Unit` have side effects without computing values.
- In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.

Equations

- Unit = PUnit

Instances For

source
@[reducible, match_pattern, inline]
abbrev Unit.unit :
Unit

The only element of the unit type.

It can be written as an empty tuple: `()`.

Equations

- () = PUnit.unit

Instances For

source
unsafe axiom lcErased :
Type

Marker for information that has been erased by the code generator.

source
unsafe axiom lcAny :
Type

Marker for type dependency that has been erased by the code generator.

source
unsafe axiom lcRealWorld :
Type

Internal representation of `IO.RealWorld` in the compiler.

source
unsafe axiom lcProof {α : Prop} :
α

Auxiliary unsafe constant used by the Compiler when erasing proofs from code.

It may look strange to have an axiom that says "every proposition is true", since this is obviously unsound, but the `unsafe` marker ensures that the kernel will not let this through into regular proofs. The lower levels of the code generator don't need proofs in terms, so this is used to stub the proofs out.

source
unsafe axiom lcCast {α : Sort u} {β : Sort v} (a : α) :
β

Auxiliary unsafe constant used by the Compiler when erasing casts.

source
unsafe axiom lcUnreachable {α : Sort u} :
α

Auxiliary unsafe constant used by the Compiler to mark unreachable code.

Like `lcProof`, this is an `unsafe axiom`, which means that even though it is not sound, the kernel will not let us use it for regular proofs.

Executing this expression to actually synthesize a value of type `α` causes immediate undefined behavior, and the compiler does take advantage of this to optimize the code assuming that it is not called. If it is not optimized out, it is likely to appear as a print message saying "unreachable code", but this behavior is not guaranteed or stable in any way.

source
inductive True :
Prop

`True` is a proposition and has only an introduction rule, `True.intro : True`. In other words, `True` is simply true, and has a canonical proof, `True.intro` For more information: Propositional Logic

- intro : True

  `True` is true, and `True.intro` (or more commonly, `trivial`) is the proof.

Instances For

source
inductive False :
Prop

`False` is the empty proposition. Thus, it has no introduction rules. It represents a contradiction. `False` elimination rule, `False.rec`, expresses the fact that anything follows from a contradiction. This rule is sometimes called ex falso (short for ex falso sequitur quodlibet), or the principle of explosion. For more information: Propositional Logic

Instances For

source
inductive Empty :
Type

The empty type. It has no constructors.

Use `Empty.elim` in contexts where a value of type `Empty` is in scope.

Instances For

source
inductive PEmpty :
Sort u

The universe-polymorphic empty type, with no constructors.

`PEmpty` can be used in any universe, but this flexibility can lead to worse error messages and more challenges with universe level unification. Prefer the type `Empty` or the proposition `False` when possible.

Instances For

source
def Not (a : Prop) :
Prop

`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`, so if your goal is `¬p` you can use `intro h` to turn the goal into `h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False` and `(hn h).elim` will prove anything. For more information: Propositional Logic

Conventions for notations in identifiers:

- The recommended spelling of `¬` in identifiers is `not`.

Equations

- (¬a) = (a → False)

Instances For

source
@[macro_inline]
def False.elim {C : Sort u} (h : False) :
C

`False.elim : False → C` says that from `False`, any desired proposition `C` holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.

The target type is actually `C : Sort u` which means it works for both propositions and types. When executed, this acts like an "unreachable" instruction: it is undefined behavior to run, but it will probably print "unreachable code". (You would need to construct a proof of false to run it anyway, which you can only do using `sorry` or unsound axioms.)

Equations

- h.elim = False.rec (fun (x : False) => C) h

Instances For

source
@[macro_inline]
def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) :
b

Anything follows from two contradictory hypotheses. Example:

    example (hp : p) (hnp : ¬p) : q := absurd hp hnp

For more information: Propositional Logic

Equations

- absurd h₁ h₂ = False.rec (fun (x : False) => b) ⋯

Instances For

source
inductive Eq {α : Sort u_1} :
α → α → Prop

The equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation.

    variable (α : Type) (a b c d : α)
    variable (hab : a = b) (hcb : c = b) (hcd : c = d)

    example : a = d :=
      Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example:

    example (α : Type) (a b : α) (p : α → Prop)
            (h1 : a = b) (h2 : p a) : p b :=
      Eq.subst h1 h2

    example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
      h1 ▸ h2

The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: Equality

Conventions for notations in identifiers:

- The recommended spelling of `=` in identifiers is `eq`.

- refl {α : Sort u_1} (a : α) : a = a

  `Eq.refl a : a = a` is reflexivity, the unique constructor of the equality type. See also `rfl`, which is usually used instead.

Instances For

source
@[match_pattern]
def rfl {α : Sort u} {a : α} :
a = a

`rfl : a = a` is the unique constructor of the equality type. This is the same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although the statement of the theorem is `a = a`, Lean will allow anything that is definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in Lean by `rfl`, because both sides are the same up to definitional equality.

Equations

- ⋯ = ⋯

Instances For

source
@[simp]
theorem id_eq {α : Sort u_1} (a : α) :
id a = a

`id x = x`, as a `@[simp]` lemma.

source
theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : a = b) (h₂ : motive a) :
motive b

The substitution principle for equality. If `a = b` and `P a` holds, then `P b` also holds. We conventionally use the name `motive` for `P` here, so that you can specify it explicitly using e.g. `Eq.subst (motive := fun x => x < 5)` if it is not otherwise inferred correctly.

This theorem is the underlying mechanism behind the `rw` tactic, which is essentially a fancy algorithm for finding good `motive` arguments to usefully apply this theorem to replace occurrences of `a` with `b` in the goal or hypotheses.

For more information: Equality

source
theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) :
b = a

Equality is symmetric: if `a = b` then `b = a`.

Because this is in the `Eq` namespace, if you have a variable `h : a = b`, `h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.

For more information: Equality

source
theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :
a = c

Equality is transitive: if `a = b` and `b = c` then `a = c`.

Because this is in the `Eq` namespace, if you have variables or expressions `h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand for `Eq.trans h₁ h₂`.

For more information: Equality

source
@[macro_inline]
def cast {α β : Sort u} (h : α = β) (a : α) :
β

Cast across a type equality. If `h : α = β` is an equality of types, and `a : α`, then `a : β` will usually not typecheck directly, but this function will allow you to work around this and embed `a` in type `β` as `cast h a : β`.

It is best to avoid this function if you can, because it is more complicated to reason about terms containing casts, but if the types don't match up definitionally sometimes there isn't anything better you can do.

For more information: Equality

Equations

- cast h a = h ▸ a

Instances For

source
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) :
f a₁ = f a₂

Congruence in the function argument: if `a₁ = a₂` then `f a₁ = f a₂` for any (nondependent) function `f`. This is more powerful than it might look at first, because you can also use a lambda expression for `f` to prove that `<something containing a₁> = <something containing a₂>`. This function is used internally by tactics like `congr` and `simp` to apply equalities inside subterms.

For more information: Equality

source
theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) :
f₁ a₁ = f₂ a₂

Congruence in both function and argument. If `f₁ = f₂` and `a₁ = a₂` then `f₁ a₁ = f₂ a₂`. This only works for nondependent functions; the theorem statement is more complex in the dependent case.

For more information: Equality

source
theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) :
f a = g a

Congruence in the function part of an application: If `f = g` then `f a = g a`.

Initialize the Quotient Module, which effectively adds the following definitions:

    opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u

    opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r

    opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
      (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β

    opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
      (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q

source
opaque Quot {α : Sort u} (r : α → α → Prop) :
Sort u

Low-level quotient types. Quotient types coarsen the propositional equality for a type `α`, so that terms related by some relation `r` are considered equal in `Quot r`.

Set-theoretically, `Quot r` can seen as the set of equivalence classes of `α` modulo `r`. Functions from `Quot r` must prove that they respect `r`: to define a function `f : Quot r → β`, it is necessary to provide `f' : α → β` and prove that for all `x : α` and `y : α`, `r x y → f' x = f' y`.

`Quot` is a built-in primitive:

- `Quot.mk` places elements of the underlying type `α` into the quotient.
- `Quot.lift` allows the definition of functions from the quotient to some other type.
- `Quot.sound` asserts the equality of elements related by `r`.
- `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed with `Quot.mk`.

The relation `r` is not required to be an equivalence relation; the resulting quotient type's equality extends `r` to an equivalence as a consequence of the rules for equality and quotients. When `r` is an equivalence relation, it can be more convenient to use the higher-level type `Quotient`.

source
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) :
Quot r

Places an element of a type into the quotient that equates terms according to the provided relation.

Given `v : α` and relation `r : α → α → Prop`, `Quot.mk r v : Quot r` is like `v`, except all observations of `v`'s value must respect `r`.

`Quot.mk` is a built-in primitive:

- `Quot` is the built-in quotient type.
- `Quot.lift` allows the definition of functions from the quotient to some other type.
- `Quot.sound` asserts the equality of elements related by `r`.
- `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed with `Quot.mk`.

source
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (mk : ∀ (a : α), β (mk r a)) (q : Quot r) :
β q

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with `Quot.mk`.

`Quot.rec` is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

`Quot.ind` is a built-in primitive:

- `Quot` is the built-in quotient type.
- `Quot.mk` places elements of the underlying type `α` into the quotient.
- `Quot.lift` allows the definition of functions from the quotient to some other type.
- `Quot.sound` asserts the equality of elements related by `r`.

source
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (a : ∀ (a b : α), r a b → f a = f b) :
Quot r → β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's relation.

Given a relation `r : α → α → Prop` and a quotient `Quot r`, applying a function `f : α → β` requires a proof `a` that `f` respects `r`. In this case, `Quot.lift f a : Quot r → β` computes the same values as `f`.

Lean's type theory includes a definitional reduction from `Quot.lift f h (Quot.mk r v)` to `f v`.

`Quot.lift` is a built-in primitive:

- `Quot` is the built-in quotient type.
- `Quot.mk` places elements of the underlying type `α` into the quotient.
- `Quot.sound` asserts the equality of elements related by `r`
- `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed with `Quot.mk`; it is analogous to the recursor for a structure.

source
unsafe axiom Quot.lcInv {α : Sort u} {r : α → α → Prop} (q : Quot r) :
α

Unsafe auxiliary constant used by the compiler to erase `Quot.lift`.

source
inductive HEq {α : Sort u} :
α → {β : Sort u} → β → Prop

Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same type, and casting `a` across the equality yields `b`, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as `Eq`, because the assumption that the types of `a` and `b` are equal is often too weak to prove theorems of interest. One public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y` and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`. (This does follow if you have `f = g` instead.) However if `a` and `b` have the same type then `a = b` and `a ≍ b` are equivalent.

Conventions for notations in identifiers:

- The recommended spelling of `≍` in identifiers is `heq`.

- refl {α : Sort u} (a : α) : a ≍ a

  Reflexivity of heterogeneous equality.

Instances For

source
@[match_pattern]
def HEq.rfl {α : Sort u} {a : α} :
a ≍ a

A version of `HEq.refl` with an implicit argument.

Equations

- ⋯ = ⋯

Instances For

source
theorem eq_of_heq {α : Sort u} {a a' : α} (h : a ≍ a') :
a = a'

If two heterogeneously equal terms have the same type, then they are propositionally equal.

source
@[unbox]
structure Prod (α : Type u) (β : Type v) :
Type (max u v)

The product type, usually written `α × β`. Product types are also called pair or tuple types. Elements of this type are pairs in which the first element is an `α` and the second element is a `β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.

Conventions for notations in identifiers:

- The recommended spelling of `×` in identifiers is `Prod`.

- fst : α

  The first element of a pair.

- snd : β

  The second element of a pair.

Instances For

source
structure PProd (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)

A product type in which the types may be propositions, usually written `α ×' β`.

This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.

Conventions for notations in identifiers:

- The recommended spelling of `×'` in identifiers is `PProd`.

- fst : α

  The first element of a pair.

- snd : β

  The second element of a pair.

Instances For

source
structure MProd (α β : Type u) :
Type u

A product type in which both `α` and `β` are in the same universe.

It is called `MProd` is because it is the universe-monomorphic product type.

- fst : α

  The first element of a pair.

- snd : β

  The second element of a pair.

Instances For

source
structure And (a b : Prop) :
Prop

`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.

Conventions for notations in identifiers:

- The recommended spelling of `∧` in identifiers is `and`.

- The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).

- intro :: (

- left : a

  Extract the left conjunct from a conjunction. `h : a ∧ b` then `h.left`, also notated as `h.1`, is a proof of `a`.

- right : b

  Extract the right conjunct from a conjunction. `h : a ∧ b` then `h.right`, also notated as `h.2`, is a proof of `b`.

- )

Instances For

source
inductive Or (a b : Prop) :
Prop

`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`, and you can use `match` or `cases` to destruct an `Or` assumption into the two cases.

Conventions for notations in identifiers:

- The recommended spelling of `∨` in identifiers is `or`.

- The recommended spelling of `\/` in identifiers is `or` (prefer `∨` over `\/`).

- inl {a b : Prop} (h : a) : a ∨ b

  `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`.

- inr {a b : Prop} (h : b) : a ∨ b

  `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`.

Instances For

source
theorem Or.intro_left {a : Prop} (b : Prop) (h : a) :
a ∨ b

Alias for `Or.inl`.

source
theorem Or.intro_right {b : Prop} (a : Prop) (h : b) :
a ∨ b

Alias for `Or.inr`.

source
theorem Or.elim {a b c : Prop} (h : a ∨ b) (left : a → c) (right : b → c) :
c

Proof by cases on an `Or`. If `a ∨ b`, and both `a` and `b` imply proposition `c`, then `c` is true.

source
theorem Or.resolve_left {a b : Prop} (h : a ∨ b) (na : ¬a) :
b
source
theorem Or.resolve_right {a b : Prop} (h : a ∨ b) (nb : ¬b) :
a
source
theorem Or.neg_resolve_left {a b : Prop} (h : ¬a ∨ b) (ha : a) :
b
source
theorem Or.neg_resolve_right {a b : Prop} (h : a ∨ ¬b) (nb : b) :
a
source
inductive Bool :
Type

The Boolean values, `true` and `false`.

Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is public important for programming: both propositions and their proofs are erased in the code generator, while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information.

- false : Bool

  The Boolean value `false`, not to be confused with the proposition `False`.

- true : Bool

  The Boolean value `true`, not to be confused with the proposition `True`.

Instances For

source
structure Subtype {α : Sort u} (p : α → Prop) :
Sort (max 1 u)

All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the underlying type is expected.

Examples:

- `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
- `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
- Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are contained in `xs`.

Conventions for notations in identifiers:

- The recommended spelling of `{ x // p x }` in identifiers is `subtype`.

- val : α

  The value in the underlying type that satisfies the predicate.

- property : p self.val

  The proof that `val` satisfies the predicate `p`.

Instances For

source
@[reducible]
def optParam (α : Sort u) (default : α) :
Sort u

Gadget for optional parameter support.

A binder like `(x : α := default)` in a declaration is syntax sugar for `x : optParam α default`, and triggers the elaborator to attempt to use `default` to supply the argument if it is not supplied.

Equations

- optParam α default = α

Instances For

source
@[reducible]
def outParam (α : 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.

Equations

- outParam α = α

Instances For

source
@[reducible]
def semiOutParam (α : 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 `α`.

Equations

- semiOutParam α = α

Instances For

source
@[reducible]
def namedPattern {α : Sort u} (x a : α) (h : x = a) :
α

Auxiliary declaration used to implement named patterns like `x@h:p`.

Equations

- a = a

Instances For

source
@[never_extract, extern lean_sorry]
axiom sorryAx (α : Sort u) (synthetic : Bool) :
α

Auxiliary axiom used to implement the `sorry` term and tactic.

The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. It is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton. Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it, but you can check if a declaration depends on `sorry` either directly or indirectly by looking for `sorryAx` in the output of the `#print axioms my_thm` command.

The `synthetic` flag is false when a `sorry` is written explicitly by the user, but it is set to `true` when a tactic fails to prove a goal, or if there is a type error in the expression. A synthetic `sorry` acts like a regular one, except that it suppresses follow-up errors in order to prevent an error from causing a cascade of other errors because the desired term was not constructed.

source
theorem eq_false_of_ne_true {b : Bool} :
¬b = true → b = false
source
theorem eq_true_of_ne_false {b : Bool} :
¬b = false → b = true
source
theorem ne_false_of_eq_true {b : Bool} :
b = true → ¬b = false
source
theorem ne_true_of_eq_false {b : Bool} :
b = false → ¬b = true
source
class Inhabited (α : 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`.

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

Instances

source
class inductive Nonempty (α : 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`.

- intro {α : Sort u} (val : α) : Nonempty α

  If `val : α`, then `α` is nonempty.

Instances

source
axiom Classical.choice {α : Sort u} :
Nonempty α → α

The axiom of choice. `Nonempty α` is a proof that `α` has an element, but the element itself is erased. The axiom `choice` supplies a particular element of `α` given only this proof.

The textbook axiom of choice normally makes a family of choices all at once, but that is implied from this formulation, because if `α : ι → Type` is a family of types and `h : ∀ i, Nonempty (α i)` is a proof that they are all nonempty, then `fun i => Classical.choice (h i) : ∀ i, α i` is a family of chosen elements. This is actually a bit stronger than the ZFC choice axiom; this is sometimes called "global choice".

In Lean, we use the axiom of choice to derive the law of excluded middle (see `Classical.em`), so it will often show up in axiom listings where you may not expect. You can use `#print axioms my_thm` to find out if a given theorem depends on this or other axioms.

This axiom can be used to construct "data", but obviously there is no algorithm to compute it, so Lean will require you to mark any definition that would involve executing `Classical.choice` or other axioms as `noncomputable`, and will not produce any executable code for such definitions.

source
theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : ∀ (a : α), p) :
p

The elimination principle for `Nonempty α`. If `Nonempty α`, and we can prove `p` given any element `x : α`, then `p` holds. Note that it is essential that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent to `Classical.choice`.

source
instance instNonemptyOfInhabited {α : Sort u} [Inhabited α] :
Nonempty α
source
noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] :
α

A variation on `Classical.choice` that uses typeclass inference to infer the proof of `Nonempty α`.

Equations

- Classical.ofNonempty = Classical.choice ⋯

Instances For

source
instance instNonemptyForall {α : Sort u} {β : Sort v} [Nonempty β] :
Nonempty (α → β)
source
instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [∀ (a : α), Nonempty (β a)] :
Nonempty ((a : α) → β a)
source
instance instInhabitedSort :
Inhabited (Sort u)
Equations

- instInhabitedSort = { default := PUnit }

source
instance instInhabitedForall (α : Sort u) {β : Sort v} [Inhabited β] :
Inhabited (α → β)
Equations

- instInhabitedForall α = { default := fun (x : α) => default }

source
instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
Inhabited ((a : α) → β a)
Equations

- Pi.instInhabited = { default := fun (x : α) => default }

source
def instInhabitedBool.default :
Bool
Equations

- instInhabitedBool.default = false

Instances For

source
instance instInhabitedBool :
Inhabited Bool
Equations

- instInhabitedBool = { default := instInhabitedBool.default }

source
structure PLift (α : Sort u) :
Type u

Lifts a proposition or type to a higher universe level.

`PLift α` wraps a proof or value of type `α`. The resulting type is in the next largest universe after that of `α`. In particular, propositions become data.

The related type `ULift` can be used to lift a non-proposition type by any number of levels.

Examples:

- `(False : Prop)`
- `(PLift False : Type)`
- `([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))`
- `(Nat : Type 0)`
- `(PLift Nat : Type 1)`

- up :: (

- down : α

  Extracts a wrapped proof or value from a universe-lifted proposition or type.

- )

Instances For

source
theorem PLift.up_down {α : Sort u} (b : PLift α) :
{ down := b.down } = b

Bijection between `α` and `PLift α`

source
theorem PLift.down_up {α : Sort u} (a : α) :
{ down := a }.down = a

Bijection between `α` and `PLift α`

source
def NonemptyType :
Type (u + 1)

`NonemptyType.{u}` is the type of nonempty types in universe `u`. It is mainly used in constant declarations where we wish to introduce a type and simultaneously assert that it is nonempty, but otherwise make the type opaque.

Equations

- NonemptyType = { α : Type ?u.3 // Nonempty α }

Instances For

source
@[reducible, inline]
abbrev NonemptyType.type (type : NonemptyType) :
Type u

The underlying type of a `NonemptyType`.

Equations

- type.type = type.val

Instances For

source
instance instInhabitedNonemptyType :
Inhabited NonemptyType

`NonemptyType` is inhabited, because `PUnit` is a nonempty type.

Equations

- instInhabitedNonemptyType = { default := ⟨PUnit, ⋯⟩ }

source
structure ULift (α : Type s) :
Type (max s r)

Lifts a type to a higher universe level.

`ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be the minimal level, it takes a further level parameter and occupies their maximum. The resulting type may occupy any universe that's at least as large as that of `α`.

The resulting universe of the lifting operator is the first parameter, and may be written explicitly while allowing `α`'s level to be inferred.

The related type `PLift` can be used to lift a proposition or type by one level.

Examples:

- `(Nat : Type 0)`
- `(ULift Nat : Type 0)`
- `(ULift Nat : Type 1)`
- `(ULift Nat : Type 5)`
- `(ULift.{7} (PUnit : Type 3) : Type 7)`

- up :: (

- down : α

  Extracts a wrapped value from a universe-lifted type.

- )

Instances For

source
theorem ULift.up_down {α : Type u} (b : ULift α) :
{ down := b.down } = b

Bijection between `α` and `ULift.{v} α`

source
theorem ULift.down_up {α : Type u} (a : α) :
{ down := a }.down = a

Bijection between `α` and `ULift.{v} α`

source
instance instInhabitedULift {α : Type u_1} [Inhabited α] :
Inhabited (ULift α)
Equations

- instInhabitedULift = { default := { down := default } }

source
structure PULift (α : Sort s) :
Sort (max s r 1)

Lifts a type or proposition to a higher universe level.

`PULift α` wraps a value of type `α`. It is a generalization of `PLift` that allows lifting values who's type may live in `Sort s`. It also subsumes `PLift`.

- up :: (

- down : α

  Extracts a wrapped value from a universe-lifted type.

- )

Instances For

source
theorem PULift.up_down {α : Sort u} (b : PULift α) :
{ down := b.down } = b

Bijection between `α` and `PULift.{v} α`

source
theorem PULift.down_up {α : Sort u} (a : α) :
{ down := a }.down = a

Bijection between `α` and `PULift.{v} α`

source
class inductive Decidable (p : Prop) :
Type

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.

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

  Proves that `p` is decidable by supplying a proof of `¬p`

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

  Proves that `p` is decidable by supplying a proof of `p`

Instances

source
@[inline_if_reduce]
def Decidable.decide (p : Prop) [h : Decidable p] :
Bool

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.

Equations

- decide p = Decidable.casesOn h (fun (x : ¬p) => false) fun (x : p) => true

Instances For

source
@[reducible, inline]
abbrev DecidablePred {α : Sort u} (r : α → Prop) :
Sort (max 1 u)

A decidable predicate.

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

Equations

- DecidablePred r = ((a : α) → Decidable (r a))

Instances For

source
@[reducible, inline]
abbrev DecidableRel {α : Sort u} {β : Sort v} (r : α → β → Prop) :
Sort (max (max 1 u) v)

A decidable relation.

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

Equations

- DecidableRel r = ((a : α) → (b : β) → Decidable (r a b))

Instances For

source
@[reducible, inline]
abbrev DecidableEq (α : Sort u) :
Sort (max 1 u)

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

Equations

- DecidableEq α = ((a b : α) → Decidable (a = b))

Instances For

source
def decEq {α : Sort u} [inst : DecidableEq α] (a b : α) :
Decidable (a = b)

Checks whether two terms of a type are equal using the type's `DecidableEq` instance.

Equations

- decEq a b = inst a b

Instances For

source
theorem decide_eq_true {p : Prop} [inst : Decidable p] :
p → decide p = true
source
theorem decide_eq_false {p : Prop} [Decidable p] :
¬p → decide p = false
source
theorem of_decide_eq_true {p : Prop} [inst : Decidable p] :
decide p = true → p
source
theorem of_decide_eq_false {p : Prop} [inst : Decidable p] :
decide p = false → ¬p
source
theorem of_decide_eq_self_eq_true {α : Sort u_1} [inst : DecidableEq α] (a : α) :
decide (a = a) = true
source
@[inline]
def Bool.decEq (a b : Bool) :
Decidable (a = b)

Decides whether two Booleans are equal.

This function should normally be called via the `DecidableEq Bool` instance that it exists to support.

Equations

- false.decEq false = isTrue ⋯
- false.decEq true = isFalse ⋯
- true.decEq false = isFalse ⋯
- true.decEq true = isTrue ⋯

Instances For

source
@[inline]
instance instDecidableEqBool :
DecidableEq Bool
Equations

- instDecidableEqBool = Bool.decEq

source
class BEq (α : 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.

- beq : α → α → Bool

  Boolean equality, notated as `a == b`.

  Conventions for notations in identifiers:

  - The recommended spelling of `==` in identifiers is `beq`.

Instances

source
@[instance 500]
instance instBEqOfDecidableEq {α : Type u_1} [DecidableEq α] :
BEq α
Equations

- instBEqOfDecidableEq = { beq := fun (a b : α) => decide (a = b) }

source
@[macro_inline]
def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬c → α) :
α

"Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`, is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as `if c then t else e` except that `t` is allowed to depend on a proof `h : c`, and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis, even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches. For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...` to avoid the bounds check inside the if branch. (Of course in this case we have only lifted the check into an explicit `if`, but we could also use this proof multiple times or derive `i < arr.size` from some other proposition that we are checking in the `if`.)

Equations

- dite c t e = Decidable.casesOn h e t

Instances For

# if-then-else #

source
@[macro_inline]
def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) :
α

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

Equations

- (if c then t else e) = Decidable.casesOn h (fun (x : ¬c) => e) fun (x : c) => t

Instances For

source
@[macro_inline]
instance instDecidableAnd {p q : Prop} [dp : Decidable p] [dq : Decidable q] :
Decidable (p ∧ q)
Equations

- instDecidableAnd = isTrue ⋯
- instDecidableAnd = isFalse ⋯
- instDecidableAnd = isFalse ⋯

source
@[macro_inline]
instance instDecidableOr {p q : Prop} [dp : Decidable p] [dq : Decidable q] :
Decidable (p ∨ q)
Equations

- instDecidableOr = isTrue ⋯
- instDecidableOr = isTrue ⋯
- instDecidableOr = isFalse ⋯

source
instance instDecidableNot {p : Prop} [dp : Decidable p] :
Decidable ¬p
Equations

- instDecidableNot = isFalse ⋯
- instDecidableNot = isTrue hq

# Boolean operators #

source
@[macro_inline]
def cond {α : Sort u} (c : Bool) (x y : α) :
α

The conditional function.

`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation `bif c then x else y`.

Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated.

Equations

- (bif true then x else y) = x
- (bif false then x else y) = y

Instances For

source
@[macro_inline]
def Bool.dcond {α : Sort u} (c : Bool) (x : c = true → α) (y : c = false → α) :
α

The dependent conditional function, in which each branch is provided with a local assumption about the condition's value. This allows the value to be used in proofs as well as for control flow.

`dcond c (fun h => x) (fun h => y)` is the same as `if h : c then x else y`, but optimized for a Boolean condition rather than a decidable proposition. Unlike the non-dependent version `cond`, there is no special notation for `dcond`.

Just like `ite`, `dite`, and `cond`, `dcond` is declared `@[macro_inline]`, which causes applications of `dcond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated. `dcond` is intended for metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not provided.

Equations

- true.dcond x_2 y_2 = x_2 ⋯
- false.dcond x_2 y_2 = y_2 ⋯

Instances For

source
@[macro_inline]
def Bool.or (x y : Bool) :
Bool

Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.

The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨` operator.

The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation: if `x` is `true` then `y` is not evaluated at runtime.

Equations

- (true || y) = true
- (false || y) = y

Instances For

source
@[macro_inline]
def Bool.and (x y : Bool) :
Bool

Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.

The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧` operator.

The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation: if `x` is `false` then `y` is not evaluated at runtime.

Conventions for notations in identifiers:

- The recommended spelling of `&&` in identifiers is `and`.

- The recommended spelling of `||` in identifiers is `or`.

Equations

- (false && y) = false
- (true && y) = y

Instances For

source
@[inline]
def Bool.not :
Bool → Bool

Boolean negation, also known as Boolean complement. `not x` can be written `!x`.

This is a function that maps the value `true` to `false` and the value `false` to `true`. The propositional connective is `Not : Prop → Prop`.

Conventions for notations in identifiers:

- The recommended spelling of `!` in identifiers is `not`.

Equations

- (!true) = false
- (!false) = true

Instances For

source
inductive Nat :
Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually GMP); at runtime, `Nat` values that are sufficiently small are unboxed.

- zero : Nat

  Zero, the smallest natural number.

  Using `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the simp normal form.

- succ (n : Nat) : Nat

  The successor of a natural number `n`.

  Using `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the simp normal form.

Instances For

source
instance instInhabitedNat :
Inhabited Nat
Equations

- instInhabitedNat = { default := Nat.zero }

source
class OfNat (α : Type u) :
Nat → Type u

The class `OfNat α n` powers the numeric literal parser. If you write `37 : α`, Lean will attempt to synthesize `OfNat α 37`, and will generate the term `(OfNat.ofNat 37 : α)`.

There is a bit of infinite regress here since the desugaring apparently still contains a literal `37` in it. The type of expressions contains a primitive constructor for "raw natural number literals", which you can directly access using the macro `nat_lit 37`. Raw number literals are always of type `Nat`. So it would be more correct to say that Lean looks for an instance of `OfNat α (nat_lit 37)`, and it generates the term `(OfNat.ofNat (nat_lit 37) : α)`.

- ofNat : α

  The `OfNat.ofNat` function is automatically inserted by the parser when the user writes a numeric literal like `1 : α`. Implementations of this typeclass can therefore customize the behavior of `n : α` based on `n` and `α`.

Instances

source
@[defaultInstance 100]
instance instOfNatNat (n : Nat) :
OfNat Nat n
Equations

- instOfNatNat n = { ofNat := n }

source
class LE (α : Type u) :
Type u

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

- le : α → α → Prop

  The less-equal relation: `x ≤ y`

  Conventions for notations in identifiers:

  - The recommended spelling of `≤` in identifiers is `le`.

  - The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).

Instances

source
class LT (α : Type u) :
Type u

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

- lt : α → α → Prop

  The less-than relation: `x < y`

  Conventions for notations in identifiers:

  - The recommended spelling of `<` in identifiers is `lt`.

Instances

source
@[reducible]
def GE.ge {α : Type u} [LE α] (a b : α) :
Prop

`a ≥ b` is an abbreviation for `b ≤ a`.

Conventions for notations in identifiers:

- The recommended spelling of `≥` in identifiers is `ge`.

- The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).

Equations

- (a ≥ b) = (b ≤ a)

Instances For

source
@[reducible]
def GT.gt {α : Type u} [LT α] (a b : α) :
Prop

`a > b` is an abbreviation for `b < a`.

Conventions for notations in identifiers:

- The recommended spelling of `>` in identifiers is `gt`.

Equations

- (a > b) = (b < a)

Instances For

source
@[reducible, inline]
abbrev DecidableLT (α : Type u) [LT α] :
Type u

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

Equations

- DecidableLT α = DecidableRel LT.lt

Instances For

source
@[reducible, inline]
abbrev DecidableLE (α : Type u) [LE α] :
Type u

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

Equations

- DecidableLE α = DecidableRel LE.le

Instances For

source
class Max (α : Type u) :
Type u

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

- max : α → α → α

  Returns the greater of its two arguments.

Instances

source
@[inline]
def maxOfLe {α : Type u_1} [LE α] [DecidableRel LE.le] :
Max α

Constructs a `Max` instance from a decidable `≤` operation.

Equations

- maxOfLe = { max := fun (x y : α) => if x ≤ y then y else x }

Instances For

source
class Min (α : Type u) :
Type u

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

- min : α → α → α

  Returns the lesser of its two arguments.

Instances

source
@[inline]
def minOfLe {α : Type u_1} [LE α] [DecidableRel LE.le] :
Min α

Constructs a `Min` instance from a decidable `≤` operation.

Equations

- minOfLe = { min := fun (x y : α) => if x ≤ y then x else y }

Instances For

source
class Trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) :
Sort (max (max (max (max (max (max 1 u) u_1) u_2) u_3) v) w)

Transitive chaining of proofs, used e.g. by `calc`.

It takes two relations `r` and `s` as "input", and produces an "output" relation `t`, with the property that `r a b` and `s b c` implies `t a c`. The `calc` tactic uses this so that when it sees a chain with `a ≤ b` and `b < c` it knows that this should be a proof of `a < c` because there is an instance `Trans (·≤·) (·<·) (·<·)`.

- trans {a : α} {b : β} {c : γ} : r a b → s b c → t a c

  Compose two proofs by transitivity, generalized over the relations involved.

Instances

source
instance instTransEq {α : Sort u_1} {γ : Sort u_2} (r : α → γ → Sort u) :
Trans Eq r r
Equations

- instTransEq r = { trans := fun {a b : α} {c : γ} (heq : a = b) (h' : r b c) => ⋯ ▸ h' }

source
instance instTransEq_1 {α : Sort u_1} {β : Sort u_2} (r : α → β → Sort u) :
Trans r Eq r
Equations

- instTransEq_1 r = { trans := fun {a : α} {b c : β} (h' : r a b) (heq : b = c) => heq ▸ h' }

source
class HAdd (α : 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 : β`.

- hAdd : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `+` in identifiers is `add`.

Instances

source
class HSub (α : 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 : β`.

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

  Conventions for notations in identifiers:

  - The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).

Instances

source
class HMul (α : 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 : β`.

- hMul : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `*` in identifiers is `mul`.

Instances

source
class HDiv (α : 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 : β`.

- 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.tdiv` (truncation rounding).
  - For `Float`, `a / 0` follows the IEEE 754 semantics for division, usually resulting in `inf` or `nan`.

  Conventions for notations in identifiers:

  - The recommended spelling of `/` in identifiers is `div`.

Instances

source
class HMod (α : 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 : β`.

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

  Conventions for notations in identifiers:

  - The recommended spelling of `%` in identifiers is `mod`.

Instances

source
class HPow (α : 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 : β`.

- hPow : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `^` in identifiers is `pow`.

Instances

source
class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

It is assumed to represent a left action in some sense. The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action. Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b` when calculating the type of the surrounding arithmetic expression and it tries to insert coercions into `b` to get some `b'` such that `a • b'` has the same type as `b'`. See the module documentation near the macro for more details.

- hSMul : α → β → γ

  `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

  Conventions for notations in identifiers:

  - The recommended spelling of `•` in identifiers is `smul`.

Instances

source
class HAppend (α : 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 : β`.

- hAppend : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `++` in identifiers is `append`.

Instances

source
class HOrElse (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

The typeclass behind the notation `a <|> b : γ` where `a : α`, `b : β`. Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the implementation so it can decide when to evaluate it.

- hOrElse : α → (Unit → β) → γ

  `a <|> b` executes `a` and returns the result, unless it fails in which case it executes and returns `b`. Because `b` is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

  Conventions for notations in identifiers:

  - The recommended spelling of `<|>` in identifiers is `orElse`.

Instances

source
class HAndThen (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

The typeclass behind the notation `a >> b : γ` where `a : α`, `b : β`. Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the implementation so it can decide when to evaluate it.

- hAndThen : α → (Unit → β) → γ

  `a >> b` executes `a`, ignores the result, and then executes `b`. If `a` fails then `b` is not executed. Because `b` is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

  Conventions for notations in identifiers:

  - The recommended spelling of `>>` in identifiers is `andThen`.

Instances

source
class HAnd (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

- hAnd : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `&&&` in identifiers is `and`.

Instances

source
class HXor (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

- hXor : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `^^^` in identifiers is `xor`.

Instances

source
class HOr (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

- hOr : α → β → γ

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

  Conventions for notations in identifiers:

  - The recommended spelling of `|||` in identifiers is `or`.

Instances

source
class HShiftLeft (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

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

  Conventions for notations in identifiers:

  - The recommended spelling of `<<<` in identifiers is `shiftLeft`.

Instances

source
class HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

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

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

  Conventions for notations in identifiers:

  - The recommended spelling of `>>>` in identifiers is `shiftRight`.

Instances

source
class Zero (α : Type u) :
Type u

A type with a zero element.

- zero : α

  The zero element of the type.

Instances

source
class One (α : Type u) :
Type u

A type with a "one" element.

- one : α

  The "one" element of the type.

Instances

source
class Add (α : Type u) :
Type u

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

- add : α → α → α

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

Instances

source
class Sub (α : Type u) :
Type u

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

- sub : α → α → α

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

Instances

source
class Mul (α : Type u) :
Type u

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

- mul : α → α → α

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

Instances

source
class Neg (α : Type u) :
Type u

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

- neg : α → α

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

  Conventions for notations in identifiers:

  - The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).

Instances

source
class Div (α : Type u) :
Type u

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

- div : α → α → α

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

Instances

source
class Inv (α : Type u) :
Type u

The notation typeclass for inverses. This enables the notation `a⁻¹ : α` where `a : α`.

- inv : α → α

  `a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent.

  Conventions for notations in identifiers:

  - The recommended spelling of `⁻¹` in identifiers is `inv`.

Instances

source
class Mod (α : Type u) :
Type u

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

- mod : α → α → α

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

Instances

source
class Dvd (α : Type u_1) :
Type u_1

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

- dvd : α → α → Prop

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

  Conventions for notations in identifiers:

  - The recommended spelling of `∣` in identifiers is `dvd`.

Instances

source
class Pow (α : 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.

- pow : α → β → α

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

Instances

source
class NatPow (α : 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.

- pow : α → Nat → α

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

Instances

source
class HomogeneousPow (α : 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.

- pow : α → α → α

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

Instances

source
class SMul (M : Type u) (α : Type v) :
Type (max u v)

Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`)

- smul : M → α → α

  `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

Instances

source
class Append (α : Type u) :
Type u

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

- append : α → α → α

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

Instances

source
class OrElse (α : Type u) :
Type u

The homogeneous version of `HOrElse`: `a <|> b : α` where `a b : α`. Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the implementation so it can decide when to evaluate it.

- orElse : α → (Unit → α) → α

  The implementation of `a <|> b : α`. See `HOrElse`.

Instances

source
class AndThen (α : Type u) :
Type u

The homogeneous version of `HAndThen`: `a >> b : α` where `a b : α`. Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the implementation so it can decide when to evaluate it.

- andThen : α → (Unit → α) → α

  The implementation of `a >> b : α`. See `HAndThen`.

Instances

source
class AndOp (α : Type u) :
Type u

The homogeneous version of `HAnd`: `a &&& b : α` where `a b : α`. (It is called `AndOp` because `And` is taken for the propositional connective.)

- and : α → α → α

  The implementation of `a &&& b : α`. See `HAnd`.

Instances

source
class XorOp (α : Type u) :
Type u

The homogeneous version of `HXor`: `a ^^^ b : α` where `a b : α`.

- xor : α → α → α

  The implementation of `a ^^^ b : α`. See `HXor`.

Instances

source
class OrOp (α : Type u) :
Type u

The homogeneous version of `HOr`: `a ||| b : α` where `a b : α`. (It is called `OrOp` because `Or` is taken for the propositional connective.)

- or : α → α → α

  The implementation of `a ||| b : α`. See `HOr`.

Instances

source
class Complement (α : Type u) :
Type u

The typeclass behind the notation `~~~a : α` where `a : α`.

- complement : α → α

  The implementation of `~~~a : α`.

  Conventions for notations in identifiers:

  - The recommended spelling of `~~~` in identifiers is `not`.

Instances

source
class ShiftLeft (α : Type u) :
Type u

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

- shiftLeft : α → α → α

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

Instances

source
class ShiftRight (α : Type u) :
Type u

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

- shiftRight : α → α → α

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

Instances

source
@[defaultInstance 1000]
instance instHAdd {α : Type u_1} [Add α] :
HAdd α α α
Equations

- instHAdd = { hAdd := fun (a b : α) => Add.add a b }

source
@[defaultInstance 1000]
instance instHSub {α : Type u_1} [Sub α] :
HSub α α α
Equations

- instHSub = { hSub := fun (a b : α) => Sub.sub a b }

source
@[defaultInstance 1000]
instance instHMul {α : Type u_1} [Mul α] :
HMul α α α
Equations

- instHMul = { hMul := fun (a b : α) => Mul.mul a b }

source
@[defaultInstance 1000]
instance instHDiv {α : Type u_1} [Div α] :
HDiv α α α
Equations

- instHDiv = { hDiv := fun (a b : α) => Div.div a b }

source
@[defaultInstance 1000]
instance instHMod {α : Type u_1} [Mod α] :
HMod α α α
Equations

- instHMod = { hMod := fun (a b : α) => Mod.mod a b }

source
@[defaultInstance 1000]
instance instHPow {α : Type u_1} {β : Type u_2} [Pow α β] :
HPow α β α
Equations

- instHPow = { hPow := fun (a : α) (b : β) => Pow.pow a b }

source
@[defaultInstance 1000]
instance instPowNat {α : Type u_1} [NatPow α] :
Pow α Nat
Equations

- instPowNat = { pow := fun (a : α) (n : Nat) => NatPow.pow a n }

source
@[defaultInstance 1000]
instance instPowOfHomogeneousPow {α : Type u_1} [HomogeneousPow α] :
Pow α α
Equations

- instPowOfHomogeneousPow = { pow := fun (a b : α) => HomogeneousPow.pow a b }

source
@[defaultInstance 1000]
instance instHSMul {α : Type u_1} {β : Type u_2} [SMul α β] :
HSMul α β β
Equations

- instHSMul = { hSMul := SMul.smul }

source
@[instance 910]
instance instSMulOfMul {α : Type u} [Mul α] :
SMul α α
Equations

- instSMulOfMul = { smul := fun (x y : α) => Mul.mul x y }

source
@[defaultInstance 1000]
instance instHAppendOfAppend {α : Type u_1} [Append α] :
HAppend α α α
Equations

- instHAppendOfAppend = { hAppend := fun (a b : α) => Append.append a b }

source
@[defaultInstance 1000]
instance instHOrElseOfOrElse {α : Type u_1} [OrElse α] :
HOrElse α α α
Equations

- instHOrElseOfOrElse = { hOrElse := fun (a : α) (b : Unit → α) => OrElse.orElse a b }

source
@[defaultInstance 1000]
instance instHAndThenOfAndThen {α : Type u_1} [AndThen α] :
HAndThen α α α
Equations

- instHAndThenOfAndThen = { hAndThen := fun (a : α) (b : Unit → α) => AndThen.andThen a b }

source
@[defaultInstance 1000]
instance instHAndOfAndOp {α : Type u_1} [AndOp α] :
HAnd α α α
Equations

- instHAndOfAndOp = { hAnd := fun (a b : α) => AndOp.and a b }

source
@[defaultInstance 1000]
instance instHXorOfXorOp {α : Type u_1} [XorOp α] :
HXor α α α
Equations

- instHXorOfXorOp = { hXor := fun (a b : α) => XorOp.xor a b }

source
@[defaultInstance 1000]
instance instHOrOfOrOp {α : Type u_1} [OrOp α] :
HOr α α α
Equations

- instHOrOfOrOp = { hOr := fun (a b : α) => OrOp.or a b }

source
@[defaultInstance 1000]
instance instHShiftLeftOfShiftLeft {α : Type u_1} [ShiftLeft α] :
HShiftLeft α α α
Equations

- instHShiftLeftOfShiftLeft = { hShiftLeft := fun (a b : α) => ShiftLeft.shiftLeft a b }

source
@[defaultInstance 1000]
instance instHShiftRightOfShiftRight {α : Type u_1} [ShiftRight α] :
HShiftRight α α α
Equations

- instHShiftRightOfShiftRight = { hShiftRight := fun (a b : α) => ShiftRight.shiftRight a b }

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

The typeclass behind the notation `a ∈ s : Prop` where `a : α`, `s : γ`. Because `α` is an `outParam`, the "container type" `γ` determines the type of the elements of the container.

- mem : γ → α → Prop

  The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`.

  Conventions for notations in identifiers:

  - The recommended spelling of `∈` in identifiers is `mem`.

Instances

source
@[match_pattern, extern lean_nat_add]
def Nat.add :
Nat → Nat → Nat

Addition of natural numbers, typically used via the `+` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Equations

- x✝.add Nat.zero = x✝
- x✝.add b.succ = (x✝.add b).succ

Instances For

source
instance instAddNat :
Add Nat
Equations

- instAddNat = { add := Nat.add }

source
@[extern lean_nat_mul]
def Nat.mul :
Nat → Nat → Nat

Multiplication of natural numbers, usually accessed via the `*` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Equations

- x✝.mul 0 = 0
- x✝.mul b.succ = (x✝.mul b).add x✝

Instances For

source
instance instMulNat :
Mul Nat
Equations

- instMulNat = { mul := Nat.mul }

source
@[extern lean_nat_pow]
def Nat.pow (m : Nat) :
Nat → Nat

The power operation on natural numbers, usually accessed via the `^` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Equations

- m.pow 0 = 1
- m.pow n.succ = (m.pow n).mul m

Instances For

source
instance instNatPowNat :
NatPow Nat
Equations

- instNatPowNat = { pow := Nat.pow }

source
@[extern lean_nat_dec_eq]
def Nat.beq :
Nat → Nat → Bool

Boolean equality of natural numbers, usually accessed via the `==` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Equations

- Nat.zero.beq Nat.zero = true
- Nat.zero.beq n.succ = false
- n.succ.beq Nat.zero = false
- n.succ.beq m.succ = n.beq m

Instances For

source
theorem Nat.eq_of_beq_eq_true {n m : Nat} :
n.beq m = true → n = m
source
theorem Nat.ne_of_beq_eq_false {n m : Nat} :
n.beq m = false → ¬n = m
source
theorem noConfusion_of_Nat {α : Sort u} (f : α → Nat) {a b : α} (h : a = b) :
Bool.rec False True ((f a).beq (f b))

A helper theorem to deduce `False` from `a = b` when `f a ≠ f b` for some function `f : α → Nat` (typically `.ctorIdx`). Used as a simpler alternative to the no-confusion theorems.

source
@[reducible, extern lean_nat_dec_eq]
def Nat.decEq (n m : Nat) :
Decidable (n = m)

A decision procedure for equality of natural numbers, usually accessed via the `DecidableEq Nat` instance.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

- `Nat.decEq 5 5 = isTrue rfl`
- `(if 3 = 4 then "yes" else "no") = "no"`
- `show 12 = 12 by decide`

Equations

- n.decEq m = match h : n.beq m with | true => isTrue ⋯ | false => isFalse ⋯

Instances For

source
@[inline]
instance instDecidableEqNat :
DecidableEq Nat
Equations

- instDecidableEqNat = Nat.decEq

source
@[extern lean_nat_dec_le]
def Nat.ble :
Nat → Nat → Bool

The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

- `Nat.ble 2 5 = true`
- `Nat.ble 5 2 = false`
- `Nat.ble 5 5 = true`

Equations

- Nat.zero.ble Nat.zero = true
- Nat.zero.ble n.succ = true
- n.succ.ble Nat.zero = false
- n.succ.ble m.succ = n.ble m

Instances For

source
inductive Nat.le (n : Nat) :
Nat → Prop

Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.

- refl {n : Nat} : n.le n

  Non-strict inequality is reflexive: `n ≤ n`

- step {n m : Nat} : n.le m → n.le m.succ

  If `n ≤ m`, then `n ≤ m + 1`.

Instances For

source
instance instLENat :
LE Nat
Equations

- instLENat = { le := Nat.le }

source
def Nat.lt (n m : Nat) :
Prop

Strict inequality of natural numbers, usually accessed via the `<` operator.

It is defined as `n < m = n + 1 ≤ m`.

Equations

- n.lt m = n.succ.le m

Instances For

source
instance instLTNat :
LT Nat
Equations

- instLTNat = { lt := Nat.lt }

source
theorem Nat.not_succ_le_zero (n : Nat) :
n.succ ≤ 0 → False
source
@[simp]
theorem Nat.not_lt_zero (n : Nat) :
¬n < 0
source
@[simp]
theorem Nat.zero_le (n : Nat) :
0 ≤ n
source
theorem Nat.succ_le_succ {n m : Nat} :
n ≤ m → n.succ ≤ m.succ
source
@[simp]
theorem Nat.zero_lt_succ (n : Nat) :
0 < n.succ
source
theorem Nat.le_step {n m : Nat} (h : n ≤ m) :
n ≤ m.succ
source
theorem Nat.le_trans {n m k : Nat} :
n ≤ m → m ≤ k → n ≤ k
source
theorem Nat.lt_of_lt_of_le {n m k : Nat} :
n < m → m ≤ k → n < k
source
theorem Nat.lt_trans {n m k : Nat} (h₁ : n < m) :
m < k → n < k
source
theorem Nat.le_succ (n : Nat) :
n ≤ n.succ
source
theorem Nat.le_succ_of_le {n m : Nat} (h : n ≤ m) :
n ≤ m.succ
source
@[simp]
theorem Nat.le_refl (n : Nat) :
n ≤ n
source
theorem Nat.succ_pos (n : Nat) :
0 < n.succ
source
@[extern lean_nat_pred]
def Nat.pred :
Nat → Nat

The predecessor of a natural number is one less than it. The predecessor of `0` is defined to be `0`.

This definition is overridden in the compiler with an efficient implementation. This definition is the logical model.

Equations

- Nat.pred 0 = 0
- n.succ.pred = n

Instances For

source
theorem Nat.pred_le_pred {n m : Nat} :
n ≤ m → n.pred ≤ m.pred
source
theorem Nat.le_of_succ_le_succ {n m : Nat} :
n.succ ≤ m.succ → n ≤ m
source
theorem Nat.le_of_lt_succ {m n : Nat} :
m < n.succ → m ≤ n
source
def Nat.eq_or_lt_of_le {n m : Nat} :
n ≤ m → n = m ∨ n < m
Equations

- ⋯ = ⋯

Instances For

source
theorem Nat.lt_or_ge (n m : Nat) :
n < m ∨ n ≥ m
source
theorem Nat.not_succ_le_self (n : Nat) :
¬n.succ ≤ n
source
@[simp]
theorem Nat.lt_irrefl (n : Nat) :
¬n < n
source
theorem Nat.lt_of_le_of_lt {n m k : Nat} (h₁ : n ≤ m) (h₂ : m < k) :
n < k
source
theorem Nat.le_antisymm {n m : Nat} (h₁ : n ≤ m) (h₂ : m ≤ n) :
n = m
source
theorem Nat.lt_of_le_of_ne {n m : Nat} (h₁ : n ≤ m) (h₂ : ¬n = m) :
n < m
source
theorem Nat.le_of_ble_eq_true {n m : Nat} (h : n.ble m = true) :
n ≤ m
source
theorem Nat.ble_self_eq_true (n : Nat) :
n.ble n = true
source
theorem Nat.ble_succ_eq_true {n m : Nat} :
n.ble m = true → n.ble m.succ = true
source
theorem Nat.ble_eq_true_of_le {n m : Nat} (h : n ≤ m) :
n.ble m = true
source
theorem Nat.not_le_of_not_ble_eq_true {n m : Nat} (h : ¬n.ble m = true) :
¬n ≤ m
source
theorem Nat.lt_succ_of_le {n m : Nat} :
n ≤ m → n < m.succ
source
@[simp]
theorem Nat.lt_add_one (n : Nat) :
n < n + 1
source
theorem Nat.lt_succ_self (n : Nat) :
n < n.succ
source
theorem Nat.lt_of_not_le {a b : Nat} (h : ¬a ≤ b) :
b < a
source
theorem Nat.add_pos_right {b : Nat} (a : Nat) (hb : 0 < b) :
0 < a + b
source
theorem Nat.mul_pos {n m : Nat} (hn : 0 < n) (hm : 0 < m) :
0 < n * m
source
theorem Nat.pow_pos {a n : Nat} (h : 0 < a) :
0 < a ^ n
source
@[extern lean_nat_dec_le]
instance Nat.decLe (n m : Nat) :
Decidable (n ≤ m)

A decision procedure for non-strict inequality of natural numbers, usually accessed via the `DecidableLE Nat` instance.

Examples:

- `(if 3 ≤ 4 then "yes" else "no") = "yes"`
- `(if 6 ≤ 4 then "yes" else "no") = "no"`
- `show 12 ≤ 12 by decide`
- `show 5 ≤ 12 by decide`

Equations

- n.decLe m = if h : n.ble m = true then isTrue ⋯ else isFalse ⋯

source
@[extern lean_nat_dec_lt]
instance Nat.decLt (n m : Nat) :
Decidable (n < m)

A decision procedure for strict inequality of natural numbers, usually accessed via the `DecidableLT Nat` instance.

Examples:

- `(if 3 < 4 then "yes" else "no") = "yes"`
- `(if 4 < 4 then "yes" else "no") = "no"`
- `(if 6 < 4 then "yes" else "no") = "no"`
- `show 5 < 12 by decide`

Equations

- n.decLt m = n.succ.decLe m

source
instance instMinNat :
Min Nat
Equations

- instMinNat = minOfLe

source
@[extern lean_nat_sub]
def Nat.sub :
Nat → Nat → Nat

Subtraction of natural numbers, truncated at `0`. Usually used via the `-` operator.

If a result would be less than zero, then the result is zero.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

- `5 - 3 = 2`
- `8 - 2 = 6`
- `8 - 8 = 0`
- `8 - 20 = 0`

Equations

- x✝.sub 0 = x✝
- x✝.sub b.succ = (x✝.sub b).pred

Instances For

source
instance instSubNat :
Sub Nat
Equations

- instSubNat = { sub := Nat.sub }

source
theorem Nat.succ_sub_succ_eq_sub (n m : Nat) :
n.succ - m.succ = n - m
source
theorem Nat.pred_le (n : Nat) :
n.pred ≤ n
source
@[simp]
theorem Nat.sub_le (n m : Nat) :
n - m ≤ n
source
theorem Nat.sub_lt {n m : Nat} :
0 < n → 0 < m → n - m < n
source
theorem Nat.div_rec_lemma {x y : Nat} :
0 < y ∧ y ≤ x → x - y < x
source
theorem Nat.div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) :
x - y < fuel
source
@[irreducible, extern lean_nat_div]
def Nat.div (x y : Nat) :
Nat

Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed via the `/` operator.

This operation is sometimes called “floor division.”

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

- `21 / 3 = 7`
- `21 / 5 = 4`
- `0 / 22 = 0`
- `5 / 0 = 0`

Equations

- x.div y = if hy : 0 < y then Nat.div.go y hy x.succ x ⋯ else 0

Instances For

source
def Nat.div.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) :
Nat
Equations

- Nat.div.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.div.go y hy fuel_2 (x - y) ⋯ + 1 else 0

Instances For

source
instance Nat.instDiv :
Div Nat
Equations

- Nat.instDiv = { div := Nat.div }

source
@[irreducible, extern lean_nat_mod]
noncomputable def Nat.modCore (x y : Nat) :
Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather than an error.

This is the core implementation of `Nat.mod`. It computes the correct result for any two closed natural numbers, but it does not have some convenient definitional reductions when the `Nat`s contain free variables. The wrapper `Nat.mod` handles those cases specially and then calls `Nat.modCore`.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Equations

- x.modCore y = if hy : 0 < y then Nat.modCore.go y hy x.succ x ⋯ else x

Instances For

source
noncomputable def Nat.modCore.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) :
Nat
Equations

- Nat.modCore.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.modCore.go y hy fuel_2 (x - y) ⋯ else x

Instances For

source
theorem Nat.modCoreGo_lt {fuel y : Nat} (hy : 0 < y) (x : Nat) (hfuel : x < fuel) :
modCore.go y hy fuel x hfuel < y
source
theorem Nat.modCore_lt {x y : Nat} (hy : 0 < y) :
x.modCore y < y
source
@[extern lean_nat_mod]
def Nat.mod :
Nat → Nat → Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather than an error.

`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better definitional reductions:

- `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
- `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.

These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses `Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore` can handle all numbers, but its definitional reductions are not as convenient.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

- `7 % 2 = 1`
- `9 % 3 = 0`
- `5 % 7 = 5`
- `5 % 0 = 5`
- `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
- `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`

Equations

- Nat.mod 0 x✝ = 0
- n.succ.mod x✝ = if x✝ ≤ n.succ then n.succ.modCore x✝ else n.succ

Instances For

source
instance Nat.instMod :
Mod Nat
Equations

- Nat.instMod = { mod := Nat.mod }

source
theorem Nat.mod_lt (x : Nat) {y : Nat} (hy : 0 < y) :
x % y < y
source
@[extern lean_system_platform_nbits]
opaque System.Platform.getNumBits :
Unit → { n : Nat // n = 32 ∨ n = 64 }

Gets the word size of the current platform. The word size may be 64 or 32 bits.

This function is opaque because there is no guarantee at compile time that the target will have the same word size as the host. It also helps avoid having type checking be architecture-dependent.

Lean only works on 64 and 32 bit systems. This fact is visible in the return type.

source
def System.Platform.numBits :
Nat

The word size of the current platform, which may be 64 or 32 bits.

Equations

- System.Platform.numBits = (System.Platform.getNumBits ()).val

Instances For

source
theorem System.Platform.numBits_eq :
numBits = 32 ∨ numBits = 64

The word size of the current platform may be 64 or 32 bits.

source
structure Fin (n : Nat) :
Type

Natural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.

- val : Nat

  The number that is strictly less than `n`.

  `Fin.val` is a coercion, so any `Fin n` can be used in a position where a `Nat` is expected.

- isLt : ↑self < n

  The number `val` is strictly less than the bound `n`.

Instances For

source
theorem Fin.eq_of_val_eq {n : Nat} {i j : Fin n} :
↑i = ↑j → i = j
source
theorem Fin.val_eq_of_eq {n : Nat} {i j : Fin n} (h : i = j) :
↑i = ↑j
source
instance instDecidableEqFin (n : Nat) :
DecidableEq (Fin n)
Equations

- instDecidableEqFin n i j = match decEq ↑i ↑j with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

source
instance instLTFin {n : Nat} :
LT (Fin n)
Equations

- instLTFin = { lt := fun (a b : Fin n) => ↑a < ↑b }

source
instance instLEFin {n : Nat} :
LE (Fin n)
Equations

- instLEFin = { le := fun (a b : Fin n) => ↑a ≤ ↑b }

source
instance Fin.decLt {n : Nat} (a b : Fin n) :
Decidable (a < b)
Equations

- a.decLt b = (↑a).decLt ↑b

source
instance Fin.decLe {n : Nat} (a b : Fin n) :
Decidable (a ≤ b)
Equations

- a.decLe b = (↑a).decLe ↑b

source
def Fin.Internal.ofNat (n : Nat) (hn : 0 < n) (a : Nat) :
Fin n

Returns `a` modulo `n` as a `Fin n`.

This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.

Equations

- Fin.Internal.ofNat n hn a = ⟨a % n, ⋯⟩

Instances For

source
structure BitVec (w : Nat) :
Type

A bitvector of the specified width.

This is represented as the underlying `Nat` number in both the runtime and the kernel, inheriting all the special support for `Nat`.

- ofFin :: (

- toFin : Fin (2 ^ w)

  Interpret a bitvector as a number less than `2^w`. O(1), because we use `Fin` as the internal representation of a bitvector.

- )

Instances For

source
def BitVec.decEq {w : Nat} (x y : BitVec w) :
Decidable (x = y)

Bitvectors have decidable equality.

This should be used via the instance `DecidableEq (BitVec w)`.

Equations

- { toFin := n }.decEq { toFin := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqBitVec {w : Nat} :
DecidableEq (BitVec w)
Equations

- instDecidableEqBitVec = BitVec.decEq

source
@[match_pattern]
def BitVec.ofNatLT {w : Nat} (i : Nat) (p : i < 2 ^ w) :
BitVec w

The `BitVec` with value `i`, given a proof that `i < 2^w`.

Equations

- i#'p = { toFin := ⟨i, p⟩ }

Instances For

source
@[match_pattern]
def BitVec.ofNat (n i : Nat) :
BitVec n

The bitvector with value `i mod 2^n`.

Conventions for notations in identifiers:

- The recommended spelling of `0#n` in identifiers is `zero` (not `ofNat_zero`).

- The recommended spelling of `1#n` in identifiers is `one` (not `ofNat_one`).

Equations

- BitVec.ofNat n i = { toFin := Fin.Internal.ofNat (2 ^ n) ⋯ i }

Instances For

source
def BitVec.toNat {w : Nat} (x : BitVec w) :
Nat

Return the underlying `Nat` that represents a bitvector.

This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.

Equations

- x.toNat = ↑x.toFin

Instances For

source
instance instLTBitVec {w : Nat} :
LT (BitVec w)
Equations

- instLTBitVec = { lt := fun (x1 x2 : BitVec w) => x1.toNat < x2.toNat }

source
instance instDecidableLtBitVec {w : Nat} (x y : BitVec w) :
Decidable (x < y)
Equations

- instDecidableLtBitVec x y = inferInstanceAs (Decidable (x.toNat < y.toNat))

source
instance instLEBitVec {w : Nat} :
LE (BitVec w)
Equations

- instLEBitVec = { le := fun (x1 x2 : BitVec w) => x1.toNat ≤ x2.toNat }

source
instance instDecidableLeBitVec {w : Nat} (x y : BitVec w) :
Decidable (x ≤ y)
Equations

- instDecidableLeBitVec x y = inferInstanceAs (Decidable (x.toNat ≤ y.toNat))

source
@[reducible, inline]
abbrev UInt8.size :
Nat

The number of distinct values representable by `UInt8`, that is, `2^8 = 256`.

Equations

- UInt8.size = 256

Instances For

source
structure UInt8 :
Type

Unsigned 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value rather than wrapping a `BitVec 8`.

- ofBitVec :: (

- toBitVec : BitVec 8

  Unpacks a `UInt8` into a `BitVec 8`. This function is overridden with a native implementation.

- )

Instances For

source
@[extern lean_uint8_of_nat]
def UInt8.ofNatLT (n : Nat) (h : n < size) :
UInt8

Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than `2^8`.

This function is overridden at runtime with an efficient implementation.

Equations

- UInt8.ofNatLT n h = { toBitVec := n#'h }

Instances For

source
@[extern lean_uint8_of_nat]
def UInt8.ofNat (n : Nat) :
UInt8

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

- `UInt8.ofNat 5 = 5`
- `UInt8.ofNat 255 = 255`
- `UInt8.ofNat 256 = 0`
- `UInt8.ofNat 259 = 3`
- `UInt8.ofNat 32770 = 2`

Equations

- UInt8.ofNat n = { toBitVec := BitVec.ofNat 8 n }

Instances For

source
@[extern lean_uint8_dec_eq]
def UInt8.decEq (a b : UInt8) :
Decidable (a = b)

Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `UInt8.decEq 123 123 = .isTrue rfl`
- `(if (6 : UInt8) = 7 then "yes" else "no") = "no"`
- `show (7 : UInt8) = 7 by decide`

Equations

- { toBitVec := n }.decEq { toBitVec := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqUInt8 :
DecidableEq UInt8
Equations

- instDecidableEqUInt8 = UInt8.decEq

source
instance instInhabitedUInt8 :
Inhabited UInt8
Equations

- instInhabitedUInt8 = { default := UInt8.ofNatLT 0 instInhabitedUInt8._proof_1 }

source
def UInt8.lt (a b : UInt8) :
Prop

Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the `<` operator.

Equations

- a.lt b = (a.toBitVec < b.toBitVec)

Instances For

source
def UInt8.le (a b : UInt8) :
Prop

Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the `≤` operator.

Equations

- a.le b = (a.toBitVec ≤ b.toBitVec)

Instances For

source
instance instLTUInt8 :
LT UInt8
Equations

- instLTUInt8 = { lt := UInt8.lt }

source
instance instLEUInt8 :
LE UInt8
Equations

- instLEUInt8 = { le := UInt8.le }

source
@[extern lean_uint8_dec_lt]
instance UInt8.decLt (a b : UInt8) :
Decidable (a < b)

Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the `DecidableLT UInt8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `(if (6 : UInt8) < 7 then "yes" else "no") = "yes"`
- `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
- `show ¬((7 : UInt8) < 7) by decide`

Equations

- a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

source
@[extern lean_uint8_dec_le]
instance UInt8.decLe (a b : UInt8) :
Decidable (a ≤ b)

Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the `DecidableLE UInt8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
- `(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"`
- `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
- `show (7 : UInt8) ≤ 7 by decide`

Equations

- a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

source
@[reducible, inline]
abbrev UInt16.size :
Nat

The number of distinct values representable by `UInt16`, that is, `2^16 = 65536`.

Equations

- UInt16.size = 65536

Instances For

source
structure UInt16 :
Type

Unsigned 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value rather than wrapping a `BitVec 16`.

- ofBitVec :: (

- toBitVec : BitVec 16

  Unpacks a `UInt16` into a `BitVec 16`. This function is overridden with a native implementation.

- )

Instances For

source
@[extern lean_uint16_of_nat]
def UInt16.ofNatLT (n : Nat) (h : n < size) :
UInt16

Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than `2^16`.

This function is overridden at runtime with an efficient implementation.

Equations

- UInt16.ofNatLT n h = { toBitVec := n#'h }

Instances For

source
@[extern lean_uint16_dec_eq]
def UInt16.decEq (a b : UInt16) :
Decidable (a = b)

Decides whether two 16-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `UInt16.decEq 123 123 = .isTrue rfl`
- `(if (6 : UInt16) = 7 then "yes" else "no") = "no"`
- `show (7 : UInt16) = 7 by decide`

Equations

- { toBitVec := n }.decEq { toBitVec := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqUInt16 :
DecidableEq UInt16
Equations

- instDecidableEqUInt16 = UInt16.decEq

source
instance instInhabitedUInt16 :
Inhabited UInt16
Equations

- instInhabitedUInt16 = { default := UInt16.ofNatLT 0 instInhabitedUInt16._proof_1 }

source
@[reducible, inline]
abbrev UInt32.size :
Nat

The number of distinct values representable by `UInt32`, that is, `2^32 = 4294967296`.

Equations

- UInt32.size = 4294967296

Instances For

source
structure UInt32 :
Type

Unsigned 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value rather than wrapping a `BitVec 32`.

- ofBitVec :: (

- toBitVec : BitVec 32

  Unpacks a `UInt32` into a `BitVec 32`. This function is overridden with a native implementation.

- )

Instances For

source
@[extern lean_uint32_of_nat]
def UInt32.ofNatLT (n : Nat) (h : n < size) :
UInt32

Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than `2^32`.

This function is overridden at runtime with an efficient implementation.

Equations

- UInt32.ofNatLT n h = { toBitVec := n#'h }

Instances For

source
@[extern lean_uint32_to_nat]
def UInt32.toNat (n : UInt32) :
Nat

Converts a 32-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

Equations

- n.toNat = n.toBitVec.toNat

Instances For

source
@[extern lean_uint32_dec_eq]
def UInt32.decEq (a b : UInt32) :
Decidable (a = b)

Decides whether two 32-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `UInt32.decEq 123 123 = .isTrue rfl`
- `(if (6 : UInt32) = 7 then "yes" else "no") = "no"`
- `show (7 : UInt32) = 7 by decide`

Equations

- { toBitVec := n }.decEq { toBitVec := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqUInt32 :
DecidableEq UInt32
Equations

- instDecidableEqUInt32 = UInt32.decEq

source
instance instInhabitedUInt32 :
Inhabited UInt32
Equations

- instInhabitedUInt32 = { default := UInt32.ofNatLT 0 instInhabitedUInt32._proof_1 }

source
instance instLTUInt32 :
LT UInt32
Equations

- instLTUInt32 = { lt := fun (a b : UInt32) => a.toBitVec < b.toBitVec }

source
instance instLEUInt32 :
LE UInt32
Equations

- instLEUInt32 = { le := fun (a b : UInt32) => a.toBitVec ≤ b.toBitVec }

source
@[extern lean_uint32_dec_lt]
instance UInt32.decLt (a b : UInt32) :
Decidable (a < b)

Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the `DecidableLT UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `(if (6 : UInt32) < 7 then "yes" else "no") = "yes"`
- `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
- `show ¬((7 : UInt32) < 7) by decide`

Equations

- a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

source
@[extern lean_uint32_dec_le]
instance UInt32.decLe (a b : UInt32) :
Decidable (a ≤ b)

Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the `DecidableLE UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
- `(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"`
- `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
- `show (7 : UInt32) ≤ 7 by decide`

Equations

- a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

source
instance instMaxUInt32 :
Max UInt32
Equations

- instMaxUInt32 = maxOfLe

source
instance instMinUInt32 :
Min UInt32
Equations

- instMinUInt32 = minOfLe

source
@[reducible, inline]
abbrev UInt64.size :
Nat

The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`.

Equations

- UInt64.size = 18446744073709551616

Instances For

source
structure UInt64 :
Type

Unsigned 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value rather than wrapping a `BitVec 64`.

- ofBitVec :: (

- toBitVec : BitVec 64

  Unpacks a `UInt64` into a `BitVec 64`. This function is overridden with a native implementation.

- )

Instances For

source
@[extern lean_uint64_of_nat]
def UInt64.ofNatLT (n : Nat) (h : n < size) :
UInt64

Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than `2^64`.

This function is overridden at runtime with an efficient implementation.

Equations

- UInt64.ofNatLT n h = { toBitVec := n#'h }

Instances For

source
@[extern lean_uint64_dec_eq]
def UInt64.decEq (a b : UInt64) :
Decidable (a = b)

Decides whether two 64-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `UInt64.decEq 123 123 = .isTrue rfl`
- `(if (6 : UInt64) = 7 then "yes" else "no") = "no"`
- `show (7 : UInt64) = 7 by decide`

Equations

- { toBitVec := n }.decEq { toBitVec := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqUInt64 :
DecidableEq UInt64
Equations

- instDecidableEqUInt64 = UInt64.decEq

source
instance instInhabitedUInt64 :
Inhabited UInt64
Equations

- instInhabitedUInt64 = { default := UInt64.ofNatLT 0 instInhabitedUInt64._proof_1 }

source
@[reducible, inline]
abbrev USize.size :
Nat

The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`.

Equations

- USize.size = 2 ^ System.Platform.numBits

Instances For

source
theorem USize.size_eq :
size = 4294967296 ∨ size = 18446744073709551616
source
theorem USize.size_pos :
0 < size
source
structure USize :
Type

Unsigned integers that are the size of a word on the platform's architecture.

On a 32-bit architecture, `USize` is equivalent to `UInt32`. On a 64-bit machine, it is equivalent to `UInt64`.

- ofBitVec :: (

- toBitVec : BitVec System.Platform.numBits

  Unpacks a `USize` into a `BitVec System.Platform.numBits`. This function is overridden with a native implementation.

- )

Instances For

source
@[extern lean_usize_of_nat]
def USize.ofNatLT (n : Nat) (h : n < size) :
USize

Converts a natural number to a `USize`. Requires a proof that the number is small enough to be representable without overflow.

This function is overridden at runtime with an efficient implementation.

Equations

- USize.ofNatLT n h = { toBitVec := n#'h }

Instances For

source
@[extern lean_usize_dec_eq]
def USize.decEq (a b : USize) :
Decidable (a = b)

Decides whether two word-sized unsigned integers are equal. Usually accessed via the `DecidableEq USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:

- `USize.decEq 123 123 = .isTrue rfl`
- `(if (6 : USize) = 7 then "yes" else "no") = "no"`
- `show (7 : USize) = 7 by decide`

Equations

- a.decEq b = match a, b with | { toBitVec := n }, { toBitVec := m } => if h : n = m then isTrue ⋯ else isFalse ⋯

Instances For

source
instance instDecidableEqUSize :
DecidableEq USize
Equations

- instDecidableEqUSize = USize.decEq

source
instance instInhabitedUSize :
Inhabited USize
Equations

- instInhabitedUSize = { default := USize.ofNatLT 0 USize.size_pos }

source
@[reducible, inline]
abbrev Nat.isValidChar (n : Nat) :
Prop

A `Nat` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a surrogate code point (the range `0xd800` to `0xdfff` inclusive).

Equations

- n.isValidChar = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

Instances For

source
@[reducible, inline]
abbrev UInt32.isValidChar (n : UInt32) :
Prop

A `UInt32` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a surrogate code point (the range `0xd800` to `0xdfff` inclusive).

Equations

- n.isValidChar = n.toNat.isValidChar

Instances For

source
structure Char :
Type

Characters are Unicode scalar values.

- val : UInt32

  The underlying Unicode scalar value as a `UInt32`.

- valid : self.val.isValidChar

  The value must be a legal scalar value.

Instances For

source
@[extern lean_uint32_of_nat]
def Char.ofNatAux (n : Nat) (h : n.isValidChar) :
Char

Pack a `Nat` encoding a valid codepoint into a `Char`. This function is overridden with a native implementation.

Equations

- Char.ofNatAux n h = { val := { toBitVec := n#'⋯ }, valid := h }

Instances For

source
@[match_pattern, noinline]
def Char.ofNat (n : Nat) :
Char

Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is returned instead.

Equations

- Char.ofNat n = if h : n.isValidChar then Char.ofNatAux n h else { val := { toBitVec := 0#'Char.ofNat._proof_1 }, valid := Char.ofNat._proof_2 }

Instances For

source
theorem Char.eq_of_val_eq {c d : Char} :
c.val = d.val → c = d
source
theorem Char.val_eq_of_eq {c d : Char} :
c = d → c.val = d.val
source
theorem Char.ne_of_val_ne {c d : Char} (h : ¬c.val = d.val) :
¬c = d
source
theorem Char.val_ne_of_ne {c d : Char} (h : ¬c = d) :
¬c.val = d.val
source
instance instDecidableEqChar :
DecidableEq Char
Equations

- instDecidableEqChar c d = match decEq c.val d.val with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

source
def Char.utf8Size (c : Char) :
Nat

Returns the number of bytes required to encode this `Char` in UTF-8.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[unbox]
inductive Option (α : Type u) :
Type u

Optional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function type, it can also represent partiality.

- none {α : Type u} : Option α

  No value.

- some {α : Type u} (val : α) : Option α

  Some value of type `α`.

Instances For

source
instance instInhabitedOption {α : Type u_1} :
Inhabited (Option α)
Equations

- instInhabitedOption = { default := none }

source
@[macro_inline]
def Option.getD {α : Type u_1} (opt : Option α) (dflt : α) :
α

Gets an optional value, returning a given default on `none`.

This function is `@[macro_inline]`, so `dflt` will not be evaluated unless `opt` turns out to be `none`.

Examples:

- `(some "hello").getD "goodbye" = "hello"`
- `none.getD "goodbye" = "goodbye"`

Equations

- (some x).getD dflt = x
- none.getD dflt = dflt

Instances For

source
@[inline]
def Option.map {α : Type u_1} {β : Type u_2} (f : α → β) :
Option α → Option β

Apply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to `List.map`. It can also be accessed via the `Functor Option` instance.

Examples:

- `(none : Option Nat).map (· + 1) = none`
- `(some 3).map (· + 1) = some 4`

Equations

- Option.map f (some x) = some (f x)
- Option.map f none = none

Instances For

source
inductive List (α : Type u) :
Type u

Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each element must be traversed to find the next element.

`List α` is isomorphic to `Array α`, but they are useful for different things:

- `List α` is easier for reasoning, and `Array α` is modeled as a wrapper around `List α`.
- `List α` works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared, `Array α` will have better performance because it can do destructive updates.

- nil {α : Type u} : List α

  The empty list, usually written `[]`.

  Conventions for notations in identifiers:

  - The recommended spelling of `[]` in identifiers is `nil`.
- cons {α : Type u} (head : α) (tail : List α) : List α

  The list whose first element is `head`, where `tail` is the rest of the list. Usually written `head :: tail`.

  Conventions for notations in identifiers:

  - The recommended spelling of `::` in identifiers is `cons`.

  - The recommended spelling of `[a]` in identifiers is `singleton`.

Instances For

source
instance instInhabitedList {α : Type u_1} :
Inhabited (List α)
Equations

- instInhabitedList = { default := [] }

source
def List.hasDecEq {α : Type u} [DecidableEq α] (a b : List α) :
Decidable (a = b)

Implements decidable equality for `List α`, assuming `α` has decidable equality.

Equations

- [].hasDecEq [] = isTrue ⋯
- (head :: tail).hasDecEq [] = isFalse ⋯
- [].hasDecEq (head :: tail) = isFalse ⋯
- (a :: as).hasDecEq (b :: bs) = match decEq a b with | isTrue hab => match as.hasDecEq bs with | isTrue habs => isTrue ⋯ | isFalse nabs => isFalse ⋯ | isFalse nab => isFalse ⋯

Instances For

source
instance instDecidableEqList {α : Type u} [DecidableEq α] :
DecidableEq (List α)
Equations

- instDecidableEqList = List.hasDecEq

source
def List.length {α : Type u_1} :
List α → Nat

The length of a list.

This function is overridden in the compiler to `lengthTR`, which uses constant stack space.

Examples:

- `([] : List String).length = 0`
- `["green", "brown"].length = 2`

Equations

- [].length = 0
- (head :: as).length = as.length + 1

Instances For

source
def List.lengthTRAux {α : Type u_1} :
List α → Nat → Nat

Auxiliary function for `List.lengthTR`.

Equations

- [].lengthTRAux x✝ = x✝
- (head :: as).lengthTRAux x✝ = as.lengthTRAux x✝.succ

Instances For

source
def List.lengthTR {α : Type u_1} (as : List α) :
Nat

The length of a list.

This is a tail-recursive version of `List.length`, used to implement `List.length` without running out of stack space.

Examples:

- `([] : List String).lengthTR = 0`
- `["green", "brown"].lengthTR = 2`

Equations

- as.lengthTR = as.lengthTRAux 0

Instances For

source
def List.get {α : Type u} (as : List α) :
Fin as.length → α

Returns the element at the provided index, counting from `0`.

In other words, for `i : Fin as.length`, `as.get i` returns the `i`'th element of the list `as`. Because the index is a `Fin` bounded by the list's length, the index will never be out of bounds.

Examples:

- `["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"`
- `["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"`

Equations

- (a :: tail).get ⟨0, isLt⟩ = a
- (head :: as).get ⟨i.succ, h⟩ = as.get ⟨i, ⋯⟩

Instances For

source
def List.set {α : Type u_1} (l : List α) (n : Nat) (a : α) :
List α

Replaces the value at (zero-based) index `n` in `l` with `a`. If the index is out of bounds, then the list is returned unmodified.

Examples:

- `["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]`
- `["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]`

Equations

- (head :: as).set 0 x✝ = x✝ :: as
- (a :: as).set n.succ x✝ = a :: as.set n x✝
- [].set x✝¹ x✝ = []

Instances For

source
@[specialize #[]]
def List.foldl {α : Type u} {β : Type v} (f : α → β → α) (init : α) :
List β → α

Folds a function over a list from the left, accumulating a value starting with `init`. The accumulated value is combined with the each element of the list in order, using `f`.

Examples:

- `[a, b, c].foldl f z = f (f (f z a) b) c`
- `[1, 2, 3].foldl (· ++ toString ·) "" = "123"`
- `[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"`

Equations

- List.foldl f x✝ [] = x✝
- List.foldl f x✝ (b :: l) = List.foldl f (f x✝ b) l

Instances For

source
def List.concat {α : Type u} :
List α → α → List α

Adds an element to the end of a list.

The added element is the last element of the resulting list.

Examples:

- `List.concat ["red", "yellow"] "green" = ["red", "yellow", "green"]`
- `List.concat [1, 2, 3] 4 = [1, 2, 3, 4]`
- `List.concat [] () = [()]`

Equations

- [].concat x✝ = [x✝]
- (a :: as).concat x✝ = a :: as.concat x✝

Instances For

source
def List.append {α : Type u_1} (xs ys : List α) :
List α

Appends two lists. Normally used via the `++` operator.

Appending lists takes time proportional to the length of the first list: `O(|xs|)`.

Examples:

- `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`.
- `[] ++ [4, 5] = [4, 5]`.
- `[1, 2, 3] ++ [] = [1, 2, 3]`.

Equations

- [].append x✝ = x✝
- (a :: as).append x✝ = a :: as.append x✝

Instances For

source
def List.flatten {α : Type u_1} :
List (List α) → List α

Concatenates a list of lists into a single list, preserving the order of the elements.

`O(|flatten L|)`.

Examples:

- `[["a"], ["b", "c"]].flatten = ["a", "b", "c"]`
- `[["a"], [], ["b", "c"], ["d", "e", "f"]].flatten = ["a", "b", "c", "d", "e", "f"]`

Equations

- [].flatten = []
- (l :: L).flatten = l.append L.flatten

Instances For

source
@[specialize #[]]
def List.map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) :
List β

Applies a function to each element of the list, returning the resulting list of values.

`O(|l|)`.

Examples:

- `[a, b, c].map f = [f a, f b, f c]`
- `[].map Nat.succ = []`
- `["one", "two", "three"].map (·.length) = [3, 3, 5]`
- `["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]`

Equations

- List.map f [] = []
- List.map f (head :: as) = f head :: List.map f as

Instances For

source
@[inline]
def List.flatMap {α : Type u} {β : Type v} (b : α → List β) (as : List α) :
List β

Applies a function that returns a list to each element of a list, and concatenates the resulting lists.

Examples:

- `[2, 3, 2].flatMap List.range = [0, 1, 0, 1, 2, 0, 1]`
- `["red", "blue"].flatMap String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']`

Equations

- List.flatMap b as = (List.map b as).flatten

Instances For

source
structure Array (α : Type u) :
Type u

`Array α` is the type of dynamic arrays with elements from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array, all updates will be performed destructively. This results in performance comparable to mutable arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while the capacity is the amount of memory currently allocated for elements. The size is accessible via `Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.

- toList : List α

  Converts an `Array α` into a `List α` that contains the same elements in the same order.

  At runtime, this is implemented by `Array.toListImpl` and is `O(n)` in the length of the array.

Instances For

source
@[reducible, match_pattern, inline]
abbrev List.toArray {α : Type u_1} (xs : List α) :
Array α

Converts a `List α` into an `Array α`.

`O(|xs|)`. At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in the length of the list. `List.toArray` should be used instead of `Array.mk`.

Examples:

- `[1, 2, 3].toArray = #[1, 2, 3]`
- `["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].`

Equations

- xs.toArray = { toList := xs }

Instances For

source
@[extern lean_mk_empty_array_with_capacity]
def Array.mkEmpty {α : Type u} (c : Nat) :
Array α

Constructs a new empty array with initial capacity `c`.

This will be deprecated in favor of `Array.emptyWithCapacity` in the future.

Equations

- Array.mkEmpty c = { toList := [] }

Instances For

source
@[extern lean_mk_empty_array_with_capacity]
def Array.emptyWithCapacity {α : Type u} (c : Nat) :
Array α

Constructs a new empty array with initial capacity `c`.

Equations

- Array.emptyWithCapacity c = { toList := [] }

Instances For

source
def Array.empty {α : Type u} :
Array α

Constructs a new empty array with initial capacity `0`.

Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.

Equations

- #[] = Array.emptyWithCapacity 0

Instances For

source
@[extern lean_array_get_size]
def Array.size {α : Type u} (a : Array α) :
Nat

Gets the number of elements stored in an array.

This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as its capacity, is at least as large as its size, but may be larger. The capacity of an array is an internal detail that's not observable by Lean code.

Equations

- a.size = a.toList.length

Instances For

source
@[extern lean_array_fget_borrowed]
unsafe opaque Array.getInternalBorrowed {α : Type u} (a : Array α) (i : Nat) (h : i < a.size) :
α

Version of `Array.getInternal` that does not increment the reference count of its result.

This is only intended for direct use by the compiler.

source
@[extern lean_array_fget]
def Array.getInternal {α : Type u} (a : Array α) (i : Nat) (h : i < a.size) :
α

Use the indexing notation `a[i]` instead.

Access an element from an array without needing a runtime bounds checks, using a `Nat` index and a proof that it is in bounds.

This function does not use `get_elem_tactic` to automatically find the proof that the index is in bounds. This is because the tactic itself needs to look up values in arrays.

Equations

- a.getInternal i h = a.toList.get ⟨i, h⟩

Instances For

source
@[reducible, inline]
abbrev Array.getD {α : Type u_1} (a : Array α) (i : Nat) (v₀ : α) :
α

Returns the element at the provided index, counting from `0`. Returns the fallback value `v₀` if the index is out of bounds.

To return an `Option` depending on whether the index is in bounds, use `a[i]?`. To panic if the index is out of bounds, use `a[i]!`.

Examples:

- `#["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"`
- `#["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"`
- `#["spring", "summer", "fall", "winter"].getD 4 "never" = "never"`

Equations

- a.getD i v₀ = if h : i < a.size then a.getInternal i h else v₀

Instances For

source
@[extern lean_array_get_borrowed]
unsafe opaque Array.get!InternalBorrowed {α : Type u} [Inhabited α] (a : Array α) (i : Nat) :
α

Version of `Array.get!Internal` that does not increment the reference count of its result.

This is only intended for direct use by the compiler.

source
@[extern lean_array_get]
def Array.get!Internal {α : Type u} [Inhabited α] (a : Array α) (i : Nat) :
α

Use the indexing notation `a[i]!` instead.

Access an element from an array, or panic if the index is out of bounds.

Equations

- a.get!Internal i = a.getD i default

Instances For

source
@[extern lean_array_push]
def Array.push {α : Type u} (a : Array α) (v : α) :
Array α

Adds an element to the end of an array. The resulting array's size is one greater than the input array. If there are no other references to the array, then it is modified in-place.

This takes amortized `O(1)` time because `Array α` is represented by a dynamic array.

Examples:

- `#[].push "apple" = #["apple"]`
- `#["apple"].push "orange" = #["apple", "orange"]`

Equations

- a.push v = { toList := a.toList.concat v }

Instances For

source
def Array.mkArray0 {α : Type u} :
Array α

Create array `#[]`

Equations

- #[] = Array.emptyWithCapacity 0

Instances For

source
def Array.mkArray1 {α : Type u} (a₁ : α) :
Array α

Create array `#[a₁]`

Equations

- #[a₁] = (Array.emptyWithCapacity 1).push a₁

Instances For

source
def Array.mkArray2 {α : Type u} (a₁ a₂ : α) :
Array α

Create array `#[a₁, a₂]`

Equations

- #[a₁, a₂] = ((Array.emptyWithCapacity 2).push a₁).push a₂

Instances For

source
def Array.mkArray3 {α : Type u} (a₁ a₂ a₃ : α) :
Array α

Create array `#[a₁, a₂, a₃]`

Equations

- #[a₁, a₂, a₃] = (((Array.emptyWithCapacity 3).push a₁).push a₂).push a₃

Instances For

source
def Array.mkArray4 {α : Type u} (a₁ a₂ a₃ a₄ : α) :
Array α

Create array `#[a₁, a₂, a₃, a₄]`

Equations

- #[a₁, a₂, a₃, a₄] = ((((Array.emptyWithCapacity 4).push a₁).push a₂).push a₃).push a₄

Instances For

source
def Array.mkArray5 {α : Type u} (a₁ a₂ a₃ a₄ a₅ : α) :
Array α

Create array `#[a₁, a₂, a₃, a₄, a₅]`

Equations

- #[a₁, a₂, a₃, a₄, a₅] = (((((Array.emptyWithCapacity 5).push a₁).push a₂).push a₃).push a₄).push a₅

Instances For

source
def Array.mkArray6 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ : α) :
Array α

Create array `#[a₁, a₂, a₃, a₄, a₅, a₆]`

Equations

- #[a₁, a₂, a₃, a₄, a₅, a₆] = ((((((Array.emptyWithCapacity 6).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆

Instances For

source
def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) :
Array α

Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇]`

Equations

- #[a₁, a₂, a₃, a₄, a₅, a₆, a₇] = (((((((Array.emptyWithCapacity 7).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇

Instances For

source
def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) :
Array α

Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈]`

Equations

- #[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈] = ((((((((Array.emptyWithCapacity 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈

Instances For

source
def Array.appendCore {α : Type u} (as bs : Array α) :
Array α

Slower `Array.append` used in quotations.

Equations

- as.appendCore bs = Array.appendCore.loop bs bs.size 0 as

Instances For

source
def Array.appendCore.loop {α : Type u} (bs : Array α) (i j : Nat) (as : Array α) :
Array α
Equations

- Array.appendCore.loop bs i j as = if hlt : j < bs.size then match i with | 0 => as | i'.succ => Array.appendCore.loop bs i' (j + 1) (as.push (bs.getInternal j hlt)) else as

Instances For

source
def Array.extract {α : Type u_1} (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
Array α

Returns the slice of `as` from indices `start` to `stop` (exclusive). The resulting array has size `(min stop as.size) - start`.

If `start` is greater or equal to `stop`, the result is empty. If `stop` is greater than the size of `as`, the size is used instead.

Examples:

- `#[0, 1, 2, 3, 4].extract 1 3 = #[1, 2]`
- `#[0, 1, 2, 3, 4].extract 1 30 = #[1, 2, 3, 4]`
- `#[0, 1, 2, 3, 4].extract 0 0 = #[]`
- `#[0, 1, 2, 3, 4].extract 2 1 = #[]`
- `#[0, 1, 2, 3, 4].extract 2 2 = #[]`
- `#[0, 1, 2, 3, 4].extract 2 3 = #[2]`
- `#[0, 1, 2, 3, 4].extract 2 4 = #[2, 3]`

Equations

- as.extract start stop = Array.extract.loop as ((min stop as.size).sub start) start (Array.emptyWithCapacity ((min stop as.size).sub start))

Instances For

source
def Array.extract.loop {α : Type u_1} (as : Array α) (i j : Nat) (bs : Array α) :
Array α
Equations

- Array.extract.loop as i j bs = if hlt : j < as.size then match i with | 0 => bs | i'.succ => Array.extract.loop as i' (j + 1) (bs.push (as.getInternal j hlt)) else bs

Instances For

source
structure ByteArray :
Type

`ByteArray` is like `Array UInt8`, but with an efficient run-time representation as a packed byte buffer.

- data : Array UInt8

  The data contained in the byte array.

  Converting between `Array` and `ByteArray` takes linear time.

Instances For

source
@[extern lean_mk_empty_byte_array]
def ByteArray.emptyWithCapacity (c : Nat) :
ByteArray

Constructs a new empty byte array with initial capacity `c`.

Equations

- ByteArray.emptyWithCapacity c = { data := #[] }

Instances For

source
def ByteArray.empty :
ByteArray

Constructs a new empty byte array with initial capacity `0`.

Use `ByteArray.emptyWithCapacity` to create an array with a greater initial capacity.

Equations

- ByteArray.empty = ByteArray.emptyWithCapacity 0

Instances For

source
@[extern lean_byte_array_push]
def ByteArray.push :
ByteArray → UInt8 → ByteArray

Adds an element to the end of an array. The resulting array's size is one greater than the input array. If there are no other references to the array, then it is modified in-place.

This takes amortized `O(1)` time because `ByteArray` is represented by a dynamic array.

Equations

- { data := bs }.push x✝ = { data := bs.push x✝ }

Instances For

source
def List.toByteArray (bs : List UInt8) :
ByteArray

Converts a list of bytes into a `ByteArray`.

Equations

- bs.toByteArray = List.toByteArray.loop bs ByteArray.empty

Instances For

source
def List.toByteArray.loop :
List UInt8 → ByteArray → ByteArray
Equations

- List.toByteArray.loop [] x✝ = x✝
- List.toByteArray.loop (b :: bs) x✝ = List.toByteArray.loop bs (x✝.push b)

Instances For

source
@[extern lean_byte_array_size]
def ByteArray.size :
ByteArray → Nat

Returns the number of bytes in the byte array.

This is the number of bytes actually in the array, as distinct from its capacity, which is the amount of memory presently allocated for the array.

Equations

- { data := bs }.size = bs.size

Instances For

source
def String.utf8EncodeChar (c : Char) :
List UInt8

Returns the sequence of bytes in a character's UTF-8 encoding.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def List.utf8Encode (l : List Char) :
ByteArray

Encode a list of characters (Unicode scalar value) in UTF-8. This is an inefficient model implementation. Use `List.asString` instead.

Equations

- l.utf8Encode = (List.flatMap String.utf8EncodeChar l).toByteArray

Instances For

source
inductive ByteArray.IsValidUTF8 (b : ByteArray) :
Prop

A byte array is valid UTF-8 if it is of the form `List.Internal.utf8Encode m` for some `m`.

Note that in order for this definition to be well-behaved it is necessary to know that this `m` is unique. To show this, one defines UTF-8 decoding and shows that encoding and decoding are mutually inverse.

- intro {b : ByteArray} (m : List Char) (hm : b = m.utf8Encode) : b.IsValidUTF8

  Show that a byte

Instances For

source
structure String :
Type

A string is a sequence of Unicode scalar values.

At runtime, strings are represented by dynamic arrays of bytes using the UTF-8 encoding. Both the size in bytes (`String.utf8ByteSize`) and in characters (`String.length`) are cached and take constant time. Many operations on strings perform in-place modifications when the reference to the string is unique.

- ofByteArray :: (

- bytes : ByteArray

  The bytes of the UTF-8 encoding of the string. Since strings have a special representation in the runtime, this function actually takes linear time and space at runtime. For efficient access to the string's bytes, use `String.utf8ByteSize` and `String.getUTF8Byte`.

- isValidUTF8 : self.bytes.IsValidUTF8

  The bytes of the string form valid UTF-8.

- )

Instances For

source
@[extern lean_string_dec_eq]
def String.decEq (s₁ s₂ : String) :
Decidable (s₁ = s₂)

Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the `=` operator.

At runtime, this function is overridden with an efficient native implementation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance instDecidableEqString :
DecidableEq String
Equations

- instDecidableEqString = String.decEq

source
structure String.Pos.Raw :
Type

A byte position in a `String`, according to its UTF-8 encoding.

Character positions (counting the Unicode code points rather than bytes) are represented by plain `Nat`s. Indexing a `String` by a `String.Pos.Raw` takes constant time, while character positions need to be translated internally to byte positions, which takes linear time.

A byte position `p` is valid for a string `s` if `0 ≤ p ≤ s.endPos` and `p` lies on a UTF-8 character boundary, see `String.Pos.IsValid`.

There is another type, `String.ValidPos`, which bundles the validity predicate. Using `String.ValidPos` instead of `String.Pos.Raw` is recommended because it will lead to less error handling and fewer edge cases.

- byteIdx : Nat

  Get the underlying byte index of a `String.Pos.Raw`

Instances For

source
instance instInhabitedRaw :
Inhabited String.Pos.Raw
Equations

- instInhabitedRaw = { default := { } }

source
instance instDecidableEqRaw :
DecidableEq String.Pos.Raw
Equations

- instDecidableEqRaw { byteIdx := b } { byteIdx := b_1 } = match decEq b b_1 with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

source
structure Substring :
Type

A region or slice of some underlying string.

A substring contains an string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many substrings of the same underlying string may exist with very little overhead, and they are more convenient than tracking the bounds by hand.

Using its constructor explicitly, it is possible to construct a `Substring` in which one or both of the positions is invalid for the string. Many operations will return unexpected or confusing results if the start and stop positions are not valid. For this reason, `Substring` will be deprecated in favor of `String.Slice`, which always represents a valid substring.

- str : String

  The underlying string.

- startPos : String.Pos.Raw

  The byte position of the start of the string slice.

- stopPos : String.Pos.Raw

  The byte position of the end of the string slice.

Instances For

source
instance instInhabitedSubstring :
Inhabited Substring
Equations

- instInhabitedSubstring = { default := { str := "", startPos := { }, stopPos := { } } }

source
@[inline]
def Substring.bsize :
Substring → Nat

The number of bytes used by the string's UTF-8 encoding.

Equations

- { str := str, startPos := b, stopPos := e }.bsize = e.byteIdx.sub b.byteIdx

Instances For

source
@[extern lean_string_utf8_byte_size]
def String.utf8ByteSize (s : String) :
Nat

The number of bytes used by the string's UTF-8 encoding.

At runtime, this function takes constant time because the byte length of strings is cached.

Equations

- s.utf8ByteSize = s.bytes.size

Instances For

source
@[inline]
def String.endPos (s : String) :
Pos.Raw

A UTF-8 byte position that points at the end of a string, just after the last character.

- `"abc".endPos = ⟨3⟩`
- `"L∃∀N".endPos = ⟨8⟩`

Equations

- s.endPos = { byteIdx := s.utf8ByteSize }

Instances For

source
@[inline]
def String.toSubstring (s : String) :
Substring

Converts a `String` into a `Substring` that denotes the entire string.

Equations

- s.toSubstring = { str := s, startPos := { }, stopPos := s.endPos }

Instances For

source
def String.toSubstring' (s : String) :
Substring

Converts a `String` into a `Substring` that denotes the entire string.

This is a version of `String.toSubstring` that doesn't have an `@[inline]` annotation.

Equations

- s.toSubstring' = s.toSubstring

Instances For

source
unsafe def unsafeCast {α : Sort u} {β : Sort v} (a : α) :
β

This function will cast a value of type `α` to type `β`, and is a no-op in the compiler. This function is extremely dangerous because there is no guarantee that types `α` and `β` have the same data representation, and this can lead to memory unsafety. It is also logically unsound, since you could just cast `True` to `False`. For all those reasons this function is marked as `unsafe`.

It is implemented by lifting both `α` and `β` into a common universe, and then using `cast (lcProof : ULift (PLift α) = ULift (PLift β))` to actually perform the cast. All these operations are no-ops in the compiler.

Using this function correctly requires some knowledge of the data representation of the source and target types. Some general classes of casts which are safe in the current runtime:

- `Array α` to `Array β` where `α` and `β` have compatible representations, or more generally for other inductive types.
- `Quot α r` and `α`.
- `@Subtype α p` and `α`, or generally any structure containing only one non-`Prop` field of type `α`.
- Casting `α` to/from `NonScalar` when `α` is a boxed generic type (i.e. a function that accepts an arbitrary type `α` and is not specialized to a scalar type like `UInt8`).

Equations

- unsafeCast a = (cast ⋯ { down := { down := a } }).down.down

Instances For

source
@[never_extract, extern lean_panic_fn]
def panicCore {α : Sort u} [Inhabited α] (msg : String) :
α

Auxiliary definition for `panic`.

Equations

- panicCore msg = default

Instances For

source
@[never_extract, noinline]
def panic {α : Sort u} [Inhabited α] (msg : String) :
α

`(panic "msg" : α)` has a built-in implementation which prints `msg` to the error buffer. It does not terminate execution, and because it is a safe function, it still has to return an element of `α`, so it takes `[Inhabited α]` and returns `default`. It is primarily intended for debugging in pure contexts, and assertion failures.

Because this is a pure function with side effects, it is marked as `@[never_extract]` so that the compiler will not perform common sub-expression elimination and other optimizations that assume that the expression is pure.

Equations

- panic msg = panicCore msg

Instances For

source
class Bind (m : Type u → Type v) :
Type (max (u + 1) v)

The `>>=` operator is overloaded via instances of `bind`.

`Bind` is typically used via `Monad`, which extends it.

- bind {α β : Type u} : m α → (α → m β) → m β

  Sequences two computations, allowing the second to depend on the value computed by the first.

  If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the result of executing `x` to get a value of type `α` and then passing it to `f`.

  Conventions for notations in identifiers:

  - The recommended spelling of `>>=` in identifiers is `bind`.

Instances

source
class Pure (f : Type u → Type v) :
Type (max (u + 1) v)

The `pure` function is overloaded via `Pure` instances.

`Pure` is typically accessed via `Monad` or `Applicative` instances.

- pure {α : Type u} : α → f α

  Given `a : α`, then `pure a : f α` represents an action that does nothing and returns `a`.

  Examples:

  - `(pure "hello" : Option String) = some "hello"`
  - `(pure "hello" : Except (Array String) String) = Except.ok "hello"`
  - `(pure "hello" : StateM Nat String).run 105 = ("hello", 105)`

Instances

source
class Functor (f : Type u → Type v) :
Type (max (u + 1) v)

A functor in the sense used in functional programming, which means a function `f : Type u → Type v` has a way of mapping a function over its contents. This `map` operator is written `<$>`, and overloaded via `Functor` instances.

This `map` function should respect identity and function composition. In other words, for all terms `v : f α`, it should be the case that:

- `id <$> v = v`

- For all functions `h : β → γ` and `g : α → β`, `(h ∘ g) <$> v = h <$> g <$> v`

While all `Functor` instances should live up to these requirements, they are not required to prove that they do. Proofs may be required or provided via the `LawfulFunctor` class.

Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of functor in the special case where the category is the category of types and functions between them.

- map {α β : Type u} : (α → β) → f α → f β

  Applies a function inside a functor. This is used to overload the `<$>` operator.

  When mapping a constant function, use `Functor.mapConst` instead, because it may be more efficient.

  Conventions for notations in identifiers:

  - The recommended spelling of `<$>` in identifiers is `map`.
- mapConst {α β : Type u} : α → f β → f α

  Mapping a constant function.

  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used.

Instances

source
class Seq (f : Type u → Type v) :
Type (max (u + 1) v)

The `<*>` operator is overloaded using the function `Seq.seq`.

While `<$>` from the class `Functor` allows an ordinary function to be mapped over its contents, `<*>` allows a function that's “inside” the functor to be applied. When thinking about `f` as possible side effects, this captures evaluation order: `seq` arranges for the effects that produce the function to occur prior to those that produce the argument value.

For most applications, `Applicative` or `Monad` should be used rather than `Seq` itself.

- seq {α β : Type u} : f (α → β) → (Unit → f α) → f β

  The implementation of the `<*>` operator.

  In a monad, `mf <*> mx` is the same as `do let f ← mf; x ← mx; pure (f x)`: it evaluates the function first, then the argument, and applies one to the other.

  To avoid surprising evaluation semantics, `mx` is taken "lazily", using a `Unit → f α` function.

  Conventions for notations in identifiers:

  - The recommended spelling of `<*>` in identifiers is `seq`.

Instances

source
class SeqLeft (f : Type u → Type v) :
Type (max (u + 1) v)

The `<*` operator is overloaded using `seqLeft`.

When thinking about `f` as potential side effects, `<*` evaluates first the left and then the right argument for their side effects, discarding the value of the right argument and returning the value of the left argument.

For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.

- seqLeft {α β : Type u} : f α → (Unit → f β) → f α

  Sequences the effects of two terms, discarding the value of the second. This function is usually invoked via the `<*` operator.

  Given `x : f α` and `y : f β`, `x <* y` runs `x`, then runs `y`, and finally returns the result of `x`.

  The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from `f`.

  Conventions for notations in identifiers:

  - The recommended spelling of `<*` in identifiers is `seqLeft`.

Instances

source
class SeqRight (f : Type u → Type v) :
Type (max (u + 1) v)

The `*>` operator is overloaded using `seqRight`.

When thinking about `f` as potential side effects, `*>` evaluates first the left and then the right argument for their side effects, discarding the value of the left argument and returning the value of the right argument.

For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.

- seqRight {α β : Type u} : f α → (Unit → f β) → f β

  Sequences the effects of two terms, discarding the value of the first. This function is usually invoked via the `*>` operator.

  Given `x : f α` and `y : f β`, `x *> y` runs `x`, then runs `y`, and finally returns the result of `y`.

  The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from `f`.

  Conventions for notations in identifiers:

  - The recommended spelling of `*>` in identifiers is `seqRight`.

Instances

source
class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f :
Type (max (u + 1) v)

An applicative functor is more powerful than a `Functor`, but less powerful than a `Monad`.

Applicative functors capture sequencing of effects with the `<*>` operator, overloaded as `seq`, but not data-dependent effects. The results of earlier computations cannot be used to control later effects.

Applicative functors should satisfy four laws. Instances of `Applicative` are not required to prove that they satisfy these laws, which are part of the `LawfulApplicative` class.

- map {α β : Type u} : (α → β) → f α → f β
- mapConst {α β : Type u} : α → f β → f α
- pure {α : Type u} : α → f α
- seq {α β : Type u} : f (α → β) → (Unit → f α) → f β
- seqLeft {α β : Type u} : f α → (Unit → f β) → f α
- seqRight {α β : Type u} : f α → (Unit → f β) → f β

Instances

source
class Monad (m : Type u → Type v) extends Applicative m, Bind m :
Type (max (u + 1) v)

Monads are an abstraction of sequential control flow and side effects used in functional programming. Monads allow both sequencing of effects and data-dependent effects: the values that result from an early step may influence the effects carried out in a later step.

The `Monad` API may be used directly. However, it is most commonly accessed through `do`-notation.

Most `Monad` instances provide implementations of `pure` and `bind`, and use default implementations for the other methods inherited from `Applicative`. Monads should satisfy certain laws, but instances are not required to prove this. An instance of `LawfulMonad` expresses that a given monad's operations are lawful.

- map {α β : Type u} : (α → β) → m α → m β
- mapConst {α β : Type u} : α → m β → m α
- pure {α : Type u} : α → m α
- seq {α β : Type u} : m (α → β) → (Unit → m α) → m β
- seqLeft {α β : Type u} : m α → (Unit → m β) → m α
- seqRight {α β : Type u} : m α → (Unit → m β) → m β
- bind {α β : Type u} : m α → (α → m β) → m β

Instances

source
instance instInhabitedForallOfMonad {α : Type u} {m : Type u → Type v} [Monad m] :
Inhabited (α → m α)
Equations

- instInhabitedForallOfMonad = { default := pure }

source
instance instInhabitedOfMonad {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] :
Inhabited (m α)
Equations

- instInhabitedOfMonad = { default := pure default }

source
instance instNonemptyOfMonad {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [Nonempty α] :
Nonempty (m α)
source
class MonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

Computations in the monad `m` can be run in the monad `n`. These translations are inserted automatically by the compiler.

Usually, `n` consists of some number of monad transformers applied to `m`, but this is not mandatory.

New instances should use this class, `MonadLift`. Clients that require one monad to be liftable into another should instead request `MonadLiftT`, which is the reflexive, transitive closure of `MonadLift`.

- monadLift {α : Type u} : m α → n α

  Translates an action from monad `m` into monad `n`.

Instances

source
class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

Computations in the monad `m` can be run in the monad `n`. These translations are inserted automatically by the compiler.

Usually, `n` consists of some number of monad transformers applied to `m`, but this is not mandatory.

This is the reflexive, transitive closure of `MonadLift`. Clients that require one monad to be liftable into another should request an instance of `MonadLiftT`. New instances should instead be defined for `MonadLift` itself.

- monadLift {α : Type u} : m α → n α

  Translates an action from monad `m` into monad `n`.

Instances

source
@[reducible, inline]
abbrev liftM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1} :
m α → n α

Translates an action from monad `m` into monad `n`.

Equations

- @liftM = @monadLift

Instances For

source
@[always_inline]
instance instMonadLiftTOfMonadLift (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [MonadLift n o] [MonadLiftT m n] :
MonadLiftT m o
Equations

- instMonadLiftTOfMonadLift m n o = { monadLift := fun {α : Type ?u.12} (x : m α) => MonadLift.monadLift (monadLift x) }

source
instance instMonadLiftT (m : Type u_1 → Type u_2) :
MonadLiftT m m
Equations

- instMonadLiftT m = { monadLift := fun {α : Type ?u.10} (x : m α) => x }

source
class MonadEval (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

Typeclass used for adapting monads. This is similar to `MonadLift`, but instances are allowed to make use of default state for the purpose of synthesizing such an instance, if necessary. Every `MonadLift` instance gives a `MonadEval` instance.

The purpose of this class is for the `#eval` command, which looks for a `MonadEval m CommandElabM` or `MonadEval m IO` instance.

- monadEval {α : Type u} : m α → n α

  Evaluates a value from monad `m` into monad `n`.

Instances

source
instance instMonadEvalOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] :
MonadEval m n
Equations

- instMonadEvalOfMonadLift = { monadEval := fun {α : Type ?u.19} => MonadLift.monadLift }

source
class MonadEvalT (m : Type u → Type v) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

The transitive closure of `MonadEval`.

- monadEval {α : Type u} : m α → n α

  Evaluates a value from monad `m` into monad `n`.

Instances

source
instance instMonadEvalTOfMonadEval (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [MonadEval n o] [MonadEvalT m n] :
MonadEvalT m o
Equations

- instMonadEvalTOfMonadEval m n o = { monadEval := fun {α : Type ?u.30} (x : m α) => MonadEval.monadEval (MonadEvalT.monadEval x) }

source
instance instMonadEvalT (m : Type u_1 → Type u_2) :
MonadEvalT m m
Equations

- instMonadEvalT m = { monadEval := fun {α : Type ?u.10} (x : m α) => x }

source
class MonadFunctor (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of as one that may change the effects in `m`, but can't do so based on specific values that are provided.

Clients of `MonadFunctor` should typically use `MonadFunctorT`, which is the reflexive, transitive closure of `MonadFunctor`. New instances should be defined for `MonadFunctor.`

- monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α

  Lifts a fully-polymorphic transformation of `m` into `n`.

Instances

source
class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) :
Type (max (max (u + 1) v) w)

A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of as one that may change the effects in `m`, but can't do so based on specific values that are provided.

This is the reflexive, transitive closure of `MonadFunctor`. It automatically chains together `MonadFunctor` instances as needed. Clients of `MonadFunctor` should typically use `MonadFunctorT`, but new instances should be defined for `MonadFunctor`.

- monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α

  Lifts a fully-polymorphic transformation of `m` into `n`.

Instances

source
@[always_inline]
instance instMonadFunctorTOfMonadFunctor (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [MonadFunctor n o] [MonadFunctorT m n] :
MonadFunctorT m o
Equations

- One or more equations did not get rendered due to their size.

source
instance monadFunctorRefl (m : Type u_1 → Type u_2) :
MonadFunctorT m m
Equations

- monadFunctorRefl m = { monadMap := fun {α : Type ?u.12} (f : {β : Type ?u.12} → m β → m β) => f }

source
@[unbox]
inductive Except (ε : Type u) (α : Type v) :
Type (max u v)

`Except ε α` is a type which represents either an error of type `ε` or a successful result with a value of type `α`.

`Except ε : Type u → Type v` is a `Monad` that represents computations that may throw exceptions: the `pure` operation is `Except.ok` and the `bind` operation returns the first encountered `Except.error`.

- error {ε : Type u} {α : Type v} : ε → Except ε α

  A failure value of type `ε`

- ok {ε : Type u} {α : Type v} : α → Except ε α

  A success value of type `α`

Instances For

source
instance instInhabitedExcept {ε : Type u} {α : Type v} [Inhabited ε] :
Inhabited (Except ε α)
Equations

- instInhabitedExcept = { default := Except.error default }

source
class MonadExceptOf (ε : semiOutParam (Type u)) (m : Type v → Type w) :
Type (max (max u (v + 1)) w)

Exception monads provide the ability to throw errors and handle errors.

In this class, `ε` is a `semiOutParam`, which means that it can influence the choice of instance. `MonadExcept ε` provides the same operations, but requires that `ε` be inferable from `m`.

`tryCatchThe`, which takes an explicit exception type, is used to desugar `try ... catch ...` steps inside `do`-blocks when the handlers have type annotations.

- throw {α : Type v} : ε → m α

  Throws an exception of type `ε` to the nearest enclosing `catch`.

- tryCatch {α : Type v} (body : m α) (handler : ε → m α) : m α

  Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.

Instances

source
@[reducible, inline]
abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) :
m α

Throws an exception, with the exception type specified explicitly. This is useful when a monad supports throwing more than one type of exception.

Use `throw` for a version that expects the exception type to be inferred from `m`.

Equations

- throwThe ε e = MonadExceptOf.throw e

Instances For

source
@[reducible, inline]
abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) :
m α

Catches errors, recovering using `handle`. The exception type is specified explicitly. This is useful when a monad supports throwing or handling more than one type of exception.

Use `tryCatch`, for a version that expects the exception type to be inferred from `m`.

Equations

- tryCatchThe ε x handle = MonadExceptOf.tryCatch x handle

Instances For

source
class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :
Type (max (max u (v + 1)) w)

Exception monads provide the ability to throw errors and handle errors.

In this class, `ε` is an `outParam`, which means that it is inferred from `m`. `MonadExceptOf ε` provides the same operations, but allows `ε` to influence instance synthesis.

`MonadExcept.tryCatch` is used to desugar `try ... catch ...` steps inside `do`-blocks when the handlers do not have exception type annotations.

- throw {α : Type v} : ε → m α

  Throws an exception of type `ε` to the nearest enclosing handler.

- tryCatch {α : Type v} (body : m α) (handler : ε → m α) : m α

  Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.

Instances

source
def MonadExcept.ofExcept {m : Type u_1 → Type u_2} {ε : Type u_3} {α : Type u_1} [Monad m] [MonadExcept ε m] :
Except ε α → m α

Re-interprets an `Except ε` action in an exception monad `m`, succeeding if it succeeds and throwing an exception if it throws an exception.

Equations

- ofExcept (Except.ok a) = pure a
- ofExcept (Except.error e) = throw e

Instances For

source
instance instMonadExceptOfMonadExceptOf (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] :
MonadExcept ε m
Equations

- instMonadExceptOfMonadExceptOf ε m = { throw := fun {α : Type ?u.18} => throwThe ε, tryCatch := fun {α : Type ?u.18} => tryCatchThe ε }

source
@[inline]
def MonadExcept.orElse {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) :
m α

Unconditional error recovery that ignores which exception was thrown. Usually used via the `<|>` operator.

If both computations throw exceptions, then the result is the second exception.

Equations

- MonadExcept.orElse t₁ t₂ = tryCatch t₁ fun (x : ε) => t₂ ()

Instances For

source
instance MonadExcept.instOrElse {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} :
OrElse (m α)
Equations

- MonadExcept.instOrElse = { orElse := MonadExcept.orElse }

source
def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max u v)

Adds the ability to access a read-only value of type `ρ` to a monad. The value can be locally overridden by `withReader`, but it cannot be mutated.

Actions in the resulting monad are functions that take the local value as a parameter, returning ordinary actions in `m`.

Equations

- ReaderT ρ m α = (ρ → m α)

Instances For

source
instance instInhabitedReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] :
Inhabited (ReaderT ρ m α)
Equations

- instInhabitedReaderT ρ m α = { default := fun (x : ρ) => default }

source
@[inline]
def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) :
m α

Executes an action from a monad with a read-only value in the underlying monad `m`.

Equations

- x.run r = x r

Instances For

source
instance ReaderT.instMonadLift {ρ : Type u} {m : Type u → Type v} :
MonadLift m (ReaderT ρ m)
Equations

- ReaderT.instMonadLift = { monadLift := fun {α : Type ?u.16} (x : m α) (x_1 : ρ) => x }

source
@[always_inline]
instance ReaderT.instMonadExceptOf {ρ : Type u} {m : Type u → Type v} (ε : Type u_1) [MonadExceptOf ε m] :
MonadExceptOf ε (ReaderT ρ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[inline]
def ReaderT.read {ρ : Type u} {m : Type u → Type v} [Monad m] :
ReaderT ρ m ρ

Retrieves the reader monad's local value. Typically accessed via `read`, or via `readThe` when more than one local value is available.

Equations

- ReaderT.read = pure

Instances For

source
@[inline]
def ReaderT.pure {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
ReaderT ρ m α

Returns the provided value `a`, ignoring the reader monad's local value. Typically used via `Pure.pure`.

Equations

- ReaderT.pure a x✝ = pure a

Instances For

source
@[inline]
def ReaderT.bind {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) :
ReaderT ρ m β

Sequences two reader monad computations. Both are provided with the local value, and the second is passed the value of the first. Typically used via the `>>=` operator.

Equations

- x.bind f r = do let a ← x r f a r

Instances For

source
@[always_inline]
instance ReaderT.instFunctorOfMonad {ρ : Type u} {m : Type u → Type v} [Monad m] :
Functor (ReaderT ρ m)
Equations

- One or more equations did not get rendered due to their size.

source
@[always_inline]
instance ReaderT.instApplicativeOfMonad {ρ : Type u} {m : Type u → Type v} [Monad m] :
Applicative (ReaderT ρ m)
Equations

- One or more equations did not get rendered due to their size.

source
instance ReaderT.instMonad {ρ : Type u} {m : Type u → Type v} [Monad m] :
Monad (ReaderT ρ m)
Equations

- ReaderT.instMonad = { toApplicative := ReaderT.instApplicativeOfMonad, bind := fun {α β : Type ?u.19} => ReaderT.bind }

source
instance ReaderT.instMonadFunctor (ρ : Type u_1) (m : Type u_1 → Type u_2) :
MonadFunctor m (ReaderT ρ m)
Equations

- ReaderT.instMonadFunctor ρ m = { monadMap := fun {α : Type ?u.19} (f : {β : Type ?u.19} → m β → m β) (x : ReaderT ρ m α) (ctx : ρ) => f (x ctx) }

source
@[inline]
def ReaderT.adapt {ρ : Type u} {m : Type u → Type v} {ρ' α : Type u} (f : ρ' → ρ) :
ReaderT ρ m α → ReaderT ρ' m α

Modifies a reader monad's local value with `f`. The resulting computation applies `f` to the incoming local value and passes the result to the inner computation.

Equations

- ReaderT.adapt f x r = x (f r)

Instances For

source
class MonadReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) :
Type v

Reader monads provide the ability to implicitly thread a value through a computation. The value can be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally overridden for a sub-computation.

In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance. `MonadReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.

- read : m ρ

  Retrieves the local value.

Instances

source
class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :
Type v

Reader monads provide the ability to implicitly thread a value through a computation. The value can be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally overridden for a sub-computation.

In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadReaderOf ρ` provides the same operations, but allows `ρ` to influence instance synthesis.

- read : m ρ

  Retrieves the local value.

  Use `readThe` to explicitly specify a type when more than one value is available.

Instances

source
@[inline]
def readThe (ρ : Type u) {m : Type u → Type v} [MonadReaderOf ρ m] :
m ρ

Retrieves the local value whose type is `ρ`. This is useful when a monad supports reading more than one type of value.

Use `read` for a version that expects the type `ρ` to be inferred from `m`.

Equations

- readThe ρ = MonadReaderOf.read

Instances For

source
instance instMonadReaderOfMonadReaderOf (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] :
MonadReader ρ m
Equations

- instMonadReaderOfMonadReaderOf ρ m = { read := readThe ρ }

source
instance instMonadReaderOfOfMonadLift {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadReaderOf ρ m] :
MonadReaderOf ρ n
Equations

- instMonadReaderOfOfMonadLift = { read := liftM read }

source
instance instMonadReaderOfReaderTOfMonad {ρ : Type u} {m : Type u → Type v} [Monad m] :
MonadReaderOf ρ (ReaderT ρ m)
Equations

- instMonadReaderOfReaderTOfMonad = { read := ReaderT.read }

source
class MonadWithReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) :
Type (max (u + 1) v)

A reader monad that additionally allows the value to be locally overridden.

In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance. `MonadWithReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.

- withReader {α : Type u} (f : ρ → ρ) (x : m α) : m α

  Locally modifies the reader monad's value while running an action.

  During the inner action `x`, reading the value returns `f` applied to the original value. After control returns from `x`, the reader monad's value is restored.

Instances

source
@[inline]
def withTheReader (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) :
m α

Locally modifies the reader monad's value while running an action, with the reader monad's local value type specified explicitly. This is useful when a monad supports reading more than one type of value.

During the inner action `x`, reading the value returns `f` applied to the original value. After control returns from `x`, the reader monad's value is restored.

Use `withReader` for a version that expects the local value's type to be inferred from `m`.

Equations

- withTheReader ρ f x = MonadWithReaderOf.withReader f x

Instances For

source
class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) :
Type (max (u + 1) v)

A reader monad that additionally allows the value to be locally overridden.

In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadWithReaderOf ρ` provides the same operations, but allows `ρ` to influence instance synthesis.

- withReader {α : Type u} (f : ρ → ρ) (x : m α) : m α

  Locally modifies the reader monad's value while running an action.

  During the inner action `x`, reading the value returns `f` applied to the original value. After control returns from `x`, the reader monad's value is restored.

Instances

source
instance instMonadWithReaderOfMonadWithReaderOf (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] :
MonadWithReader ρ m
Equations

- instMonadWithReaderOfMonadWithReaderOf ρ m = { withReader := fun {α : Type ?u.17} => withTheReader ρ }

source
instance instMonadWithReaderOfOfMonadFunctor {ρ : Type u} {m n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] :
MonadWithReaderOf ρ n
Equations

- instMonadWithReaderOfOfMonadFunctor = { withReader := fun {α : Type ?u.28} (f : ρ → ρ) => monadMap fun {β : Type ?u.28} => withTheReader ρ f }

source
instance instMonadWithReaderOfReaderT {ρ : Type u} {m : Type u → Type v} :
MonadWithReaderOf ρ (ReaderT ρ m)
Equations

- instMonadWithReaderOfReaderT = { withReader := fun {α : Type ?u.18} (f : ρ → ρ) (x : ReaderT ρ m α) (ctx : ρ) => x (f ctx) }

source
class MonadStateOf (σ : semiOutParam (Type u)) (m : Type u → Type v) :
Type (max (u + 1) v)

State monads provide a value of a given type (the state) that can be retrieved or replaced. Instances may implement these operations by passing state values around, by using a mutable reference cell (e.g. `ST.Ref σ`), or in other ways.

In this class, `σ` is a `semiOutParam`, which means that it can influence the choice of instance. `MonadState σ` provides the same operations, but requires that `σ` be inferable from `m`.

The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike local mutable state in `do`-notation.

- get : m σ

  Retrieves the current value of the monad's mutable state.

- set : σ → m PUnit

  Replaces the current value of the mutable state with a new one.

- modifyGet {α : Type u} : (σ → α × σ) → m α

  Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

  It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Instances

source
@[reducible, inline]
abbrev getThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] :
m σ

Gets the current state that has the explicitly-provided type `σ`. When the current monad has multiple state types available, this function selects one of them.

Equations

- getThe σ = MonadStateOf.get

Instances For

source
@[reducible, inline]
abbrev modifyThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → σ) :
m PUnit

Mutates the current state that has the explicitly-provided type `σ`, replacing its value with the result of applying `f` to it. When the current monad has multiple state types available, this function selects one of them.

It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Equations

- modifyThe σ f = MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)

Instances For

source
@[reducible, inline]
abbrev modifyGetThe {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → α × σ) :
m α

Applies a function to the current state that has the explicitly-provided type `σ`. The function both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← getThe σ); set s; pure a`. However, using `modifyGetThe` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Equations

- modifyGetThe σ f = MonadStateOf.modifyGet f

Instances For

source
class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :
Type (max (u + 1) v)

State monads provide a value of a given type (the state) that can be retrieved or replaced. Instances may implement these operations by passing state values around, by using a mutable reference cell (e.g. `ST.Ref σ`), or in other ways.

In this class, `σ` is an `outParam`, which means that it is inferred from `m`. `MonadStateOf σ` provides the same operations, but allows `σ` to influence instance synthesis.

The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike local mutable state in `do`-notation.

- get : m σ

  Retrieves the current value of the monad's mutable state.

- set : σ → m PUnit

  Replaces the current value of the mutable state with a new one.

- modifyGet {α : Type u} : (σ → α × σ) → m α

  Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

  It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Instances

source
instance instMonadStateOfMonadStateOf (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] :
MonadState σ m
Equations

- instMonadStateOfMonadStateOf σ m = { get := getThe σ, set := set, modifyGet := fun {α : Type ?u.19} (f : σ → α × σ) => MonadStateOf.modifyGet f }

source
@[inline]
def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) :
m PUnit

Mutates the current state, replacing its value with the result of applying `f` to it.

Use `modifyThe` to explicitly select a state type to modify.

It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Equations

- modify f = modifyGet fun (s : σ) => (PUnit.unit, f s)

Instances For

source
@[inline]
def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) :
m σ

Replaces the state with the result of applying `f` to it. Returns the old value of the state.

It is equivalent to `get <* modify f` but may be more efficient.

Equations

- getModify f = modifyGet fun (s : σ) => (s, f s)

Instances For

source
@[always_inline]
instance instMonadStateOfOfMonadLift {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadStateOf σ m] :
MonadStateOf σ n
Equations

- instMonadStateOfOfMonadLift = { get := liftM MonadStateOf.get, set := fun (s : σ) => liftM (set s), modifyGet := fun {α : Type ?u.30} (f : σ → α × σ) => monadLift (modifyGet f) }

source
inductive EStateM.Result (ε σ α : Type u) :
Type u

The value returned from a combined state and exception monad in which exceptions do not automatically roll back the state.

`Result ε σ α` is equivalent to `Except ε α × σ`, but using a single combined inductive type yields a more efficient data representation.

- ok {ε σ α : Type u} : α → σ → Result ε σ α

  A success value of type `α` and a new state `σ`.

- error {ε σ α : Type u} : ε → σ → Result ε σ α

  An exception of type `ε` and a new state `σ`.

Instances For

source
instance EStateM.instInhabitedResult {ε σ α : Type u} [Inhabited ε] [Inhabited σ] :
Inhabited (Result ε σ α)
Equations

- EStateM.instInhabitedResult = { default := EStateM.Result.error default default }

source
def EStateM (ε σ α : Type u) :
Type u

A combined state and exception monad in which exceptions do not automatically roll back the state.

Instances of `EStateM.Backtrackable` provide a way to roll back some part of the state if needed.

`EStateM ε σ` is equivalent to `ExceptT ε (StateM σ)`, but it is more efficient.

Equations

- EStateM ε σ α = (σ → EStateM.Result ε σ α)

Instances For

source
instance EStateM.instInhabited {ε σ α : Type u} [Inhabited ε] :
Inhabited (EStateM ε σ α)
Equations

- EStateM.instInhabited = { default := fun (s : σ) => EStateM.Result.error default s }

source
@[inline]
def EStateM.pure {ε σ α : Type u} (a : α) :
EStateM ε σ α

Returns a value without modifying the state or throwing an exception.

Equations

- EStateM.pure a s = EStateM.Result.ok a s

Instances For

source
@[inline]
def EStateM.set {ε σ : Type u} (s : σ) :
EStateM ε σ PUnit

Replaces the current value of the mutable state with a new one.

Equations

- EStateM.set s x✝ = EStateM.Result.ok PUnit.unit s

Instances For

source
@[inline]
def EStateM.get {ε σ : Type u} :
EStateM ε σ σ

Retrieves the current value of the monad's mutable state.

Equations

- EStateM.get s = EStateM.Result.ok s s

Instances For

source
@[inline]
def EStateM.modifyGet {ε σ α : Type u} (f : σ → α × σ) :
EStateM ε σ α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Equations

- EStateM.modifyGet f s = match f s with | (a, s) => EStateM.Result.ok a s

Instances For

source
@[inline]
def EStateM.throw {ε σ α : Type u} (e : ε) :
EStateM ε σ α

Throws an exception of type `ε` to the nearest enclosing handler.

Equations

- EStateM.throw e s = EStateM.Result.error e s

Instances For

source
class EStateM.Backtrackable (δ : outParam (Type u)) (σ : Type u) :
Type u

Exception handlers in `EStateM` save some part of the state, determined by `δ`, and restore it if an exception is caught. By default, `δ` is `Unit`, and no information is saved.

- save : σ → δ

  Extracts the information in the state that should be rolled back if an exception is handled.

- restore : σ → δ → σ

  Updates the current state with the saved information that should be rolled back. This updated state becomes the current state when an exception is handled.

Instances

source
@[inline]
def EStateM.tryCatch {ε σ δ : Type u} [Backtrackable δ σ] {α : Type u} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) :
EStateM ε σ α

Handles exceptions thrown in the combined error and state monad.

The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running `x`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit` is used, and no information is rolled back.

Equations

- x.tryCatch handle s = match x s with | EStateM.Result.error e s_1 => handle e (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s)) | ok => ok

Instances For

source
@[inline]
def EStateM.orElse {ε σ α δ : Type u} [Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) :
EStateM ε σ α

Failure handling that does not depend on specific exception values.

The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running `x₁`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit` is used, and no information is rolled back.

Equations

- x₁.orElse x₂ s = match x₁ s with | EStateM.Result.error a s_1 => x₂ () (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s)) | ok => ok

Instances For

source
@[inline]
def EStateM.adaptExcept {ε σ α ε' : Type u} (f : ε → ε') (x : EStateM ε σ α) :
EStateM ε' σ α

Transforms exceptions with a function, doing nothing on successful results.

Equations

- EStateM.adaptExcept f x s = match x s with | EStateM.Result.error e s => EStateM.Result.error (f e) s | EStateM.Result.ok a s => EStateM.Result.ok a s

Instances For

source
@[inline]
def EStateM.bind {ε σ α β : Type u} (x : EStateM ε σ α) (f : α → EStateM ε σ β) :
EStateM ε σ β

Sequences two `EStateM ε σ` actions, passing the returned value from the first into the second.

Equations

- x.bind f s = match x s with | EStateM.Result.ok a s => f a s | EStateM.Result.error e s => EStateM.Result.error e s

Instances For

source
@[inline]
def EStateM.map {ε σ α β : Type u} (f : α → β) (x : EStateM ε σ α) :
EStateM ε σ β

Transforms the value returned from an `EStateM ε σ` action using a function.

Equations

- EStateM.map f x s = match x s with | EStateM.Result.ok a s => EStateM.Result.ok (f a) s | EStateM.Result.error e s => EStateM.Result.error e s

Instances For

source
@[inline]
def EStateM.seqRight {ε σ α β : Type u} (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) :
EStateM ε σ β

Sequences two `EStateM ε σ` actions, running `x` before `y`. The first action's return value is ignored.

Equations

- x.seqRight y s = match x s with | EStateM.Result.ok a s => y () s | EStateM.Result.error e s => EStateM.Result.error e s

Instances For

source
@[always_inline]
instance EStateM.instMonad {ε σ : Type u} :
Monad (EStateM ε σ)
Equations

- One or more equations did not get rendered due to their size.

source
instance EStateM.instOrElseOfBacktrackable {ε σ α δ : Type u} [Backtrackable δ σ] :
OrElse (EStateM ε σ α)
Equations

- EStateM.instOrElseOfBacktrackable = { orElse := EStateM.orElse }

source
instance EStateM.instMonadStateOf {ε σ : Type u} :
MonadStateOf σ (EStateM ε σ)
Equations

- EStateM.instMonadStateOf = { get := EStateM.get, set := EStateM.set, modifyGet := fun {α : Type ?u.12} => EStateM.modifyGet }

source
instance EStateM.instMonadExceptOfOfBacktrackable {ε σ δ : Type u} [Backtrackable δ σ] :
MonadExceptOf ε (EStateM ε σ)
Equations

- EStateM.instMonadExceptOfOfBacktrackable = { throw := fun {α : Type ?u.23} => EStateM.throw, tryCatch := fun {α : Type ?u.23} => EStateM.tryCatch }

source
@[inline]
def EStateM.run {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) :
Result ε σ α

Executes an `EStateM` action with the initial state `s`. The returned value includes the final state and indicates whether an exception was thrown or a value was returned.

Equations

- x.run s = x s

Instances For

source
@[inline]
def EStateM.run' {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) :
Option α

Executes an `EStateM` with the initial state `s` for the returned value `α`, discarding the final state. Returns `none` if an unhandled exception was thrown.

Equations

- x.run' s = match x.run s with | EStateM.Result.ok v a => some v | EStateM.Result.error a a_1 => none

Instances For

source
@[inline]
def EStateM.dummySave {σ : Type u} :
σ → PUnit

The `save` implementation for `Backtrackable PUnit σ`.

Equations

- EStateM.dummySave x✝ = PUnit.unit

Instances For

source
@[inline]
def EStateM.dummyRestore {σ : Type u} :
σ → PUnit → σ

The `restore` implementation for `Backtrackable PUnit σ`.

Equations

- EStateM.dummyRestore s x✝ = s

Instances For

source
instance EStateM.nonBacktrackable {σ : Type u} :
Backtrackable PUnit σ

A fallback `Backtrackable` instance that saves no information from a state. This allows every type to be used as a state in `EStateM`, with no rollback.

Because this is the first declared instance of `Backtrackable _ σ`, it will be picked only if there are no other `Backtrackable _ σ` instances registered.

Equations

- EStateM.nonBacktrackable = { save := EStateM.dummySave, restore := EStateM.dummyRestore }

source
class Hashable (α : Sort u) :
Sort (max 1 u)

Types that can be hashed into a `UInt64`.

- hash : α → UInt64

  Hashes a value into a `UInt64`.

Instances

source
@[extern lean_uint64_mix_hash]
opaque mixHash (u₁ u₂ : UInt64) :
UInt64

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

source
instance instHashableSubtype {α : Sort u_1} [Hashable α] {p : α → Prop} :
Hashable (Subtype p)
Equations

- instHashableSubtype = { hash := fun (a : Subtype p) => hash a.val }

source
@[extern lean_string_hash]
opaque String.hash (s : String) :
UInt64

Computes a hash for strings.

source
instance instHashableString :
Hashable String
Equations

- instHashableString = { hash := String.hash }

source
@[implemented_by Lean.Name.hash._override]
noncomputable def Lean.Name.hash :
Name → UInt64

A hash function for names, which is stored inside the name itself as a computed field.

Equations

- Lean.Name.anonymous.hash = UInt64.ofNatLT 1723 Lean.Name.hash._proof_1✝
- (p.str s).hash = mixHash p.hash s.hash
- (p.num v).hash = mixHash p.hash (if h : v < UInt64.size then UInt64.ofNatLT v h else UInt64.ofNatLT 17 Lean.Name.hash._proof_2✝)

Instances For

source
inductive Lean.Name :
Type

Hierarchical names consist of a sequence of components, each of which is either a string or numeric, that are written separated by dots (`.`).

Hierarchical names are used to name declarations and for creating unique identifiers for free variables and metavariables.

You can create hierarchical names using a backtick:

    `Lean.Meta.whnf

It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.

You can use double backticks to request Lean to statically check whether the name corresponds to a Lean declaration in scope.

    ``Lean.Meta.whnf

If the name is not in scope, Lean will report an error.

There are two ways to convert a `String` to a `Name`:

1. `Name.mkSimple` creates a name with a single string component.

2. `String.toName` first splits the string into its dot-separated components, and then creates a hierarchical name.

- anonymous : Name

  The "anonymous" name.

- str (pre : Name) (str : String) : Name

  A string name. The name `Lean.Meta.run` is represented at

      .str (.str (.str .anonymous "Lean") "Meta") "run"

- num (pre : Name) (i : Nat) : Name

  A numerical name. This kind of name is used, for example, to create hierarchical names for free variables and metavariables. The identifier `_uniq.231` is represented as

      .num (.str .anonymous "_uniq") 231

Instances For

source
instance Lean.instInhabitedName :
Inhabited Name
Equations

- Lean.instInhabitedName = { default := Lean.Name.anonymous }

source
instance Lean.instHashableName :
Hashable Name
Equations

- Lean.instHashableName = { hash := Lean.Name.hash }

source
@[reducible, inline, export lean_name_mk_string]
abbrev Lean.Name.mkStr (p : Name) (s : String) :
Name

`.str p s` is now the preferred form.

Equations

- p.mkStr s = p.str s

Instances For

source
@[reducible, inline, export lean_name_mk_numeral]
abbrev Lean.Name.mkNum (p : Name) (v : Nat) :
Name

`.num p v` is now the preferred form.

Equations

- p.mkNum v = p.num v

Instances For

source
@[reducible, inline]
abbrev Lean.Name.mkSimple (s : String) :
Name

Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.

This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.

Equations

- Lean.Name.mkSimple s = Lean.Name.anonymous.str s

Instances For

source
@[reducible]
def Lean.Name.mkStr1 (s₁ : String) :
Name

Make name `s₁`

Equations

- Lean.Name.mkStr1 s₁ = Lean.Name.anonymous.str s₁

Instances For

source
@[reducible]
def Lean.Name.mkStr2 (s₁ s₂ : String) :
Name

Make name `s₁.s₂`

Equations

- Lean.Name.mkStr2 s₁ s₂ = (Lean.Name.anonymous.str s₁).str s₂

Instances For

source
@[reducible]
def Lean.Name.mkStr3 (s₁ s₂ s₃ : String) :
Name

Make name `s₁.s₂.s₃`

Equations

- Lean.Name.mkStr3 s₁ s₂ s₃ = ((Lean.Name.anonymous.str s₁).str s₂).str s₃

Instances For

source
@[reducible]
def Lean.Name.mkStr4 (s₁ s₂ s₃ s₄ : String) :
Name

Make name `s₁.s₂.s₃.s₄`

Equations

- Lean.Name.mkStr4 s₁ s₂ s₃ s₄ = (((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄

Instances For

source
@[reducible]
def Lean.Name.mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) :
Name

Make name `s₁.s₂.s₃.s₄.s₅`

Equations

- Lean.Name.mkStr5 s₁ s₂ s₃ s₄ s₅ = ((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅

Instances For

source
@[reducible]
def Lean.Name.mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) :
Name

Make name `s₁.s₂.s₃.s₄.s₅.s₆`

Equations

- Lean.Name.mkStr6 s₁ s₂ s₃ s₄ s₅ s₆ = (((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅).str s₆

Instances For

source
@[reducible]
def Lean.Name.mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) :
Name

Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇`

Equations

- Lean.Name.mkStr7 s₁ s₂ s₃ s₄ s₅ s₆ s₇ = ((((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅).str s₆).str s₇

Instances For

source
@[reducible]
def Lean.Name.mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) :
Name

Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈`

Equations

- Lean.Name.mkStr8 s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ = (((((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅).str s₆).str s₇).str s₈

Instances For

source
@[extern lean_name_eq]
def Lean.Name.beq :
Name → Name → Bool

(Boolean) equality comparator for names.

Equations

- Lean.Name.anonymous.beq Lean.Name.anonymous = true
- (p₁.str s₁).beq (p₂.str s₂) = (s₁ == s₂ && p₁.beq p₂)
- (p₁.num n₁).beq (p₂.num n₂) = (n₁ == n₂ && p₁.beq p₂)
- x✝¹.beq x✝ = false

Instances For

source
instance Lean.Name.instBEq :
BEq Name
Equations

- Lean.Name.instBEq = { beq := Lean.Name.beq }

source
def Lean.Name.appendCore :
Name → Name → Name

This function does not have special support for macro scopes. See `Name.append`.

Equations

- x✝.appendCore Lean.Name.anonymous = x✝
- x✝.appendCore (p.str s) = (x✝.appendCore p).str s
- x✝.appendCore (p.num d) = (x✝.appendCore p).num d

Instances For

source
def Lean.defaultMaxRecDepth :
Nat

The default maximum recursion depth. This is adjustable using the `maxRecDepth` option.

Equations

- Lean.defaultMaxRecDepth = 512

Instances For

source
def Lean.maxRecDepthErrorMessage :
String

The message to display on stack overflow.

Equations

- Lean.maxRecDepthErrorMessage = "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"

Instances For

# Syntax #

source
inductive Lean.SourceInfo :
Type

Source information that relates syntax to the context that it came from.

The primary purpose of `SourceInfo` is to relate the output of the parser and the macro expander to the original source file. When produced by the parser, `Syntax.node` does not carry source info; the parser associates it only with atoms and identifiers. If a `Syntax.node` is introduced by a quotation, then it has synthetic source info that both associates it with an original reference position and indicates that the original atoms in it may not originate from the Lean file under elaboration.

Source info is also used to relate Lean's output to the internal data that it represents; this is the basis for many interactive features. When used this way, it can occur on `Syntax.node` as well.

- original (leading : Substring) (pos : String.Pos.Raw) (trailing : Substring) (endPos : String.Pos.Raw) : SourceInfo

  A token produced by the parser from original input that includes both leading and trailing whitespace as well as position information.

  The `leading` whitespace is inferred after parsing by `Syntax.updateLeading`. This is because the “preceding token” is not well-defined during parsing, especially in the presence of backtracking.

- synthetic (pos endPos : String.Pos.Raw) (canonical : Bool := false) : SourceInfo

  Synthetic syntax is syntax that was produced by a metaprogram or by Lean itself (e.g. by a quotation). Synthetic syntax is annotated with a source span from the original syntax, which relates it to the source file.

  The delaborator uses this constructor to store an encoded indicator of which core language expression gave rise to the syntax.

  The `canonical` flag on synthetic syntax is enabled for syntax that is not literally part of the original input syntax but should be treated “as if” the user really wrote it for the purpose of hovers and error messages. This is usually used on identifiers in order to connect the binding site to the user's original syntax even if the name of the identifier changes during expansion, as well as on tokens that should receive targeted messages.

  Generally speaking, a macro expansion should only use a given piece of input syntax in a single canonical token. An exception to this rule is when the same identifier is used to declare two binders, as in the macro expansion for dependent if:

      `(if $h : $cond then $t else $e) ~>
      `(dite $cond (fun $h => $t) (fun $h => $t))

  In these cases, if the user hovers over `h` they will see information about both binding sites.

- none : SourceInfo

  A synthesized token without position information.

Instances For

source
instance Lean.instInhabitedSourceInfo :
Inhabited SourceInfo
Equations

- Lean.instInhabitedSourceInfo = { default := Lean.SourceInfo.none }

source
def Lean.SourceInfo.getPos? (info : SourceInfo) (canonicalOnly : Bool := false) :
Option String.Pos.Raw

Gets the position information from a `SourceInfo`, if available. If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false` will also return `none`.

Equations

- (Lean.SourceInfo.original leading pos trailing endPos).getPos? canonicalOnly = some pos
- (Lean.SourceInfo.synthetic pos endPos true).getPos? canonicalOnly = some pos
- (Lean.SourceInfo.synthetic pos endPos canonical).getPos? = some pos
- info.getPos? canonicalOnly = none

Instances For

source
def Lean.SourceInfo.getTailPos? (info : SourceInfo) (canonicalOnly : Bool := false) :
Option String.Pos.Raw

Gets the end position information from a `SourceInfo`, if available. If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false` will also return `none`.

Equations

- (Lean.SourceInfo.original leading pos trailing endPos).getTailPos? canonicalOnly = some endPos
- (Lean.SourceInfo.synthetic pos endPos true).getTailPos? canonicalOnly = some endPos
- (Lean.SourceInfo.synthetic pos endPos canonical).getTailPos? = some endPos
- info.getTailPos? canonicalOnly = none

Instances For

source
def Lean.SourceInfo.getTrailing? (info : SourceInfo) :
Option Substring

Gets the substring representing the trailing whitespace of a `SourceInfo`, if available.

Equations

- (Lean.SourceInfo.original leading pos trailing endPos).getTrailing? = some trailing
- info.getTrailing? = none

Instances For

source
def Lean.SourceInfo.getTrailingTailPos? (info : SourceInfo) (canonicalOnly : Bool := false) :
Option String.Pos.Raw

Gets the end position information of the trailing whitespace of a `SourceInfo`, if available. If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false` will also return `none`.

Equations

- info.getTrailingTailPos? canonicalOnly = match info.getTrailing? with | some trailing => some trailing.stopPos | none => info.getTailPos? canonicalOnly

Instances For

source
@[reducible, inline]
abbrev Lean.SyntaxNodeKind :
Type

Specifies the interpretation of a `Syntax.node` value. An abbreviation for `Name`.

Node kinds may be any name, and do not need to refer to declarations in the environment. Conventionally, however, a node's kind corresponds to the `Parser` or `ParserDesc` declaration that produces it. There are also a number of built-in node kinds that are used by the parsing infrastructure, such as `nullKind` and `choiceKind`; these do not correspond to parser declarations.

Equations

- Lean.SyntaxNodeKind = Lean.Name

Instances For

# Syntax AST #

source
inductive Lean.Syntax.Preresolved :
Type

A possible binding of an identifier in the context in which it was quoted.

Identifiers in quotations may refer to either global declarations or to namespaces that are in scope at the site of the quotation. These are saved in the `Syntax.ident` constructor and are part of the implementation of hygienic macros.

- namespace (ns : Name) : Preresolved

  A potential namespace reference

- decl (n : Name) (fields : List String) : Preresolved

  A potential global constant or section variable reference, with additional field accesses

Instances For

source
inductive Lean.Syntax :
Type

Lean syntax trees.

Syntax trees are used pervasively throughout Lean: they are produced by the parser, transformed by the macro expander, and elaborated. They are also produced by the delaborator and presented to users.

- missing : Syntax

  A portion of the syntax tree that is missing because of a parse error.

  The indexing operator on `Syntax` also returns `Syntax.missing` when the index is out of bounds.

- node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax

  A node in the syntax tree that may have further syntax as child nodes. The node's `kind` determines its interpretation.

  For nodes produced by the parser, the `info` field is typically `Lean.SourceInfo.none`, and source information is stored in the corresponding fields of identifiers and atoms. This field is used in two ways:

  1. The delaborator uses it to associate nodes with metadata that are used to implement interactive features.
  2. Nodes created by quotations use the field to mark the syntax as synthetic (storing the result of `Lean.SourceInfo.fromRef`) even when its leading or trailing tokens are not.
- atom (info : SourceInfo) (val : String) : Syntax

  A non-identifier atomic component of syntax.

  All of the following are atoms:

  - keywords, such as `def`, `fun`, and `inductive`
  - literals, such as numeric or string literals
  - punctuation and delimiters, such as `(`, `)`, and `=>`.

  Identifiers are represented by the `Lean.Syntax.ident` constructor. Atoms also correspond to quoted strings inside `syntax` declarations.

- ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Preresolved) : Syntax

  An identifier.

  In addition to source information, identifiers have the following fields:

  - `rawVal` is the literal substring from the input file
  - `val` is the parsed Lean name, potentially including macro scopes.
  - `preresolved` is the list of possible declarations this could refer to, populated by quotations.

Instances For

source
def Lean.Syntax.node1 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ : Syntax) :
Syntax

Create syntax node with 1 child

Equations

- Lean.Syntax.node1 info kind a₁ = Lean.Syntax.node info kind #[a₁]

Instances For

source
def Lean.Syntax.node2 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ : Syntax) :
Syntax

Create syntax node with 2 children

Equations

- Lean.Syntax.node2 info kind a₁ a₂ = Lean.Syntax.node info kind #[a₁, a₂]

Instances For

source
def Lean.Syntax.node3 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ : Syntax) :
Syntax

Create syntax node with 3 children

Equations

- Lean.Syntax.node3 info kind a₁ a₂ a₃ = Lean.Syntax.node info kind #[a₁, a₂, a₃]

Instances For

source
def Lean.Syntax.node4 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a₄ : Syntax) :
Syntax

Create syntax node with 4 children

Equations

- Lean.Syntax.node4 info kind a₁ a₂ a₃ a₄ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄]

Instances For

source
def Lean.Syntax.node5 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a₄ a₅ : Syntax) :
Syntax

Create syntax node with 5 children

Equations

- Lean.Syntax.node5 info kind a₁ a₂ a₃ a₄ a₅ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅]

Instances For

source
def Lean.Syntax.node6 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a₄ a₅ a₆ : Syntax) :
Syntax

Create syntax node with 6 children

Equations

- Lean.Syntax.node6 info kind a₁ a₂ a₃ a₄ a₅ a₆ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅, a₆]

Instances For

source
def Lean.Syntax.node7 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Syntax) :
Syntax

Create syntax node with 7 children

Equations

- Lean.Syntax.node7 info kind a₁ a₂ a₃ a₄ a₅ a₆ a₇ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅, a₆, a₇]

Instances For

source
def Lean.Syntax.node8 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Syntax) :
Syntax

Create syntax node with 8 children

Equations

- Lean.Syntax.node8 info kind a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈]

Instances For

source
def Lean.SyntaxNodeKinds :
Type

`SyntaxNodeKinds` is a set of `SyntaxNodeKind`, implemented as a list.

Singleton `SyntaxNodeKinds` are extremely common. They are written as name literals, rather than as lists; list syntax is required only for empty or non-singleton sets of kinds.

Equations

- Lean.SyntaxNodeKinds = List Lean.SyntaxNodeKind

Instances For

source
structure Lean.TSyntax (ks : SyntaxNodeKinds) :
Type

Typed syntax, which tracks the potential kinds of the `Syntax` it contains.

While syntax quotations produce or expect `TSyntax` values of the correct kinds, this is not otherwise enforced; it can easily be circumvented by direct use of the constructor.

- raw : Syntax

  The underlying `Syntax` value.

Instances For

source
instance Lean.instInhabitedSyntax :
Inhabited Syntax
Equations

- Lean.instInhabitedSyntax = { default := Lean.Syntax.missing }

source
instance Lean.instInhabitedTSyntax {ks : SyntaxNodeKinds} :
Inhabited (TSyntax ks)
Equations

- Lean.instInhabitedTSyntax = { default := { raw := default } }

# Builtin kinds #

source
@[reducible, inline]
abbrev Lean.choiceKind :
SyntaxNodeKind

The ``choice` kind is used to represent ambiguous parse results.

The parser prioritizes longer matches over shorter ones, but there is not always a unique longest match. All the parse results are saved, and the determination of which to use is deferred until typing information is available.

Equations

- Lean.choiceKind = `choice

Instances For

source
@[reducible, inline]
abbrev Lean.nullKind :
SyntaxNodeKind

``null` is the “fallback” kind, used when no other kind applies. Null nodes result from repetition operators, and empty null nodes represent the failure of an optional parse.

The null kind is used for raw list parsers like `many`.

Equations

- Lean.nullKind = `null

Instances For

source
@[reducible, inline]
abbrev Lean.groupKind :
SyntaxNodeKind

The ``group` kind is used for nodes that result from `Lean.Parser.group`. This avoids confusion with the null kind when used inside `optional`.

Equations

- Lean.groupKind = `group

Instances For

source
@[reducible, inline]
abbrev Lean.identKind :
SyntaxNodeKind

The pseudo-kind assigned to identifiers: ``ident`.

The name ``ident` is not actually used as a kind for `Syntax.node` values. It is used by convention as the kind of `Syntax.ident` values.

Equations

- Lean.identKind = `ident

Instances For

source
@[reducible, inline]
abbrev Lean.strLitKind :
SyntaxNodeKind

``str` is the node kind of string literals like `"foo"`.

Equations

- Lean.strLitKind = `str

Instances For

source
@[reducible, inline]
abbrev Lean.charLitKind :
SyntaxNodeKind

``char` is the node kind of character literals like `'A'`.

Equations

- Lean.charLitKind = `char

Instances For

source
@[reducible, inline]
abbrev Lean.numLitKind :
SyntaxNodeKind

``num` is the node kind of number literals like `42` and `0xa1`

Equations

- Lean.numLitKind = `num

Instances For

source
@[reducible, inline]
abbrev Lean.hexnumKind :
SyntaxNodeKind

``hexnum` is the node kind of hexadecimal numbers like `ea10` without the `0x` prefix. Recall that `hexnum` is not a token and must be prefixed. For hexadecimal number literals, you should use `num` instead. Example: `syntax anchor := "#" noWs hexnum`.

Equations

- Lean.hexnumKind = `hexnum

Instances For

source
@[reducible, inline]
abbrev Lean.scientificLitKind :
SyntaxNodeKind

``scientific` is the node kind of floating point literals like `1.23e-3`.

Equations

- Lean.scientificLitKind = `scientific

Instances For

source
@[reducible, inline]
abbrev Lean.nameLitKind :
SyntaxNodeKind

``name` is the node kind of name literals like ``foo`.

Equations

- Lean.nameLitKind = `name

Instances For

source
@[reducible, inline]
abbrev Lean.fieldIdxKind :
SyntaxNodeKind

``fieldIdx` is the node kind of projection indices like the `2` in `x.2`.

Equations

- Lean.fieldIdxKind = `fieldIdx

Instances For

source
@[reducible, inline]
abbrev Lean.hygieneInfoKind :
SyntaxNodeKind

``hygieneInfo` is the node kind of the `Lean.Parser.hygieneInfo` parser, which produces an “invisible token” that captures the hygiene information at the current point without parsing anything.

They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`) as if they were introduced in a macro's input, rather than by its implementation.

Equations

- Lean.hygieneInfoKind = `hygieneInfo

Instances For

source
@[reducible, inline]
abbrev Lean.interpolatedStrLitKind :
SyntaxNodeKind

``interpolatedStrLitKind` is the node kind of interpolated string literal fragments like `"value = {` and `}"` in `s!"value = {x}"`.

Equations

- Lean.interpolatedStrLitKind = `interpolatedStrLitKind

Instances For

source
@[reducible, inline]
abbrev Lean.interpolatedStrKind :
SyntaxNodeKind

``interpolatedStrKind` is the node kind of an interpolated string literal like `"value = {x}"` in `s!"value = {x}"`.

Equations

- Lean.interpolatedStrKind = `interpolatedStrKind

Instances For

source
@[inline]
def Lean.mkNode (k : SyntaxNodeKind) (args : Array Syntax) :
TSyntax k

Creates an info-less node of the given kind and children.

Equations

- Lean.mkNode k args = { raw := Lean.Syntax.node Lean.SourceInfo.none k args }

Instances For

source
@[inline]
def Lean.mkNullNode (args : Array Syntax := #[]) :
Syntax

Creates an info-less `nullKind` node with the given children, if any.

Equations

- Lean.mkNullNode args = (Lean.mkNode Lean.nullKind args).raw

Instances For

source
def Lean.Syntax.getKind (stx : Syntax) :
SyntaxNodeKind

Gets the kind of a `Syntax.node` value, or the pseudo-kind of any other `Syntax` value.

“Pseudo-kinds” are kinds that are assigned by convention to non-`Syntax.node` values: `identKind` for `Syntax.ident`, ``missing` for `Syntax.missing`, and the atom's string literal for atoms.

Equations

- (Lean.Syntax.node info k args).getKind = k
- Lean.Syntax.missing.getKind = `missing
- (Lean.Syntax.atom info v).getKind = Lean.Name.mkSimple v
- (Lean.Syntax.ident info rawVal val preresolved).getKind = Lean.identKind

Instances For

source
def Lean.Syntax.setKind (stx : Syntax) (k : SyntaxNodeKind) :
Syntax

Changes the kind at the root of a `Syntax.node` to `k`.

Returns all other `Syntax` values unchanged.

Equations

- (Lean.Syntax.node info kind args).setKind k = Lean.Syntax.node info k args
- stx.setKind k = stx

Instances For

source
def Lean.Syntax.isOfKind (stx : Syntax) (k : SyntaxNodeKind) :
Bool

Checks whether syntax has the given kind or pseudo-kind.

“Pseudo-kinds” are kinds that are assigned by convention to non-`Syntax.node` values: `identKind` for `Syntax.ident`, ``missing` for `Syntax.missing`, and the atom's string literal for atoms.

Equations

- stx.isOfKind k = (stx.getKind == k)

Instances For

source
def Lean.Syntax.getArg (stx : Syntax) (i : Nat) :
Syntax

Gets the `i`'th argument of the syntax node. This can also be written `stx[i]`. Returns `missing` if `i` is out of range.

Equations

- (Lean.Syntax.node info kind args).getArg i = args.getD i Lean.Syntax.missing
- stx.getArg i = Lean.Syntax.missing

Instances For

source
def Lean.Syntax.getArgs (stx : Syntax) :
Array Syntax

Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`.

Equations

- (Lean.Syntax.node info kind args).getArgs = args
- stx.getArgs = #[]

Instances For

source
def Lean.Syntax.getNumArgs (stx : Syntax) :
Nat

Gets the number of arguments of the syntax node, or `0` if it's not a `node`.

Equations

- (Lean.Syntax.node info kind args).getNumArgs = args.size
- stx.getNumArgs = 0

Instances For

source
def Lean.Syntax.getOptional? (stx : Syntax) :
Option Syntax

Assuming `stx` was parsed by `optional`, returns the enclosed syntax if it parsed something and `none` otherwise.

Equations

- (Lean.Syntax.node info kind args).getOptional? = match kind == Lean.nullKind && args.size == 1 with | true => some (args.get!Internal 0) | false => none
- stx.getOptional? = none

Instances For

source
def Lean.Syntax.isMissing :
Syntax → Bool

Is this syntax `.missing`?

Equations

- Lean.Syntax.missing.isMissing = true
- x✝.isMissing = false

Instances For

source
def Lean.Syntax.isNodeOf (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) :
Bool

Is this syntax a `node` with kind `k`?

Equations

- stx.isNodeOf k n = (stx.isOfKind k && stx.getNumArgs == n)

Instances For

source
def Lean.Syntax.isIdent :
Syntax → Bool

`stx.isIdent` is `true` iff `stx` is an identifier.

Equations

- (Lean.Syntax.ident info rawVal val preresolved).isIdent = true
- x✝.isIdent = false

Instances For

source
def Lean.Syntax.getId :
Syntax → Name

If this is an `ident`, return the parsed value, else `.anonymous`.

Equations

- (Lean.Syntax.ident info rawVal val preresolved).getId = val
- x✝.getId = Lean.Name.anonymous

Instances For

source
def Lean.Syntax.getInfo? :
Syntax → Option SourceInfo

Retrieve the immediate info from the Syntax node.

Equations

- (Lean.Syntax.atom info val).getInfo? = some info
- (Lean.Syntax.ident info rawVal val preresolved).getInfo? = some info
- (Lean.Syntax.node info kind args).getInfo? = some info
- Lean.Syntax.missing.getInfo? = none

Instances For

source
partial def Lean.Syntax.getHeadInfo? :
Syntax → Option SourceInfo

Retrieve the left-most node or leaf's info in the Syntax tree.

source
def Lean.Syntax.getHeadInfo (stx : Syntax) :
SourceInfo

Retrieve the left-most leaf's info in the Syntax tree, or `none` if there is no token.

Equations

- stx.getHeadInfo = match stx.getHeadInfo? with | some info => info | none => Lean.SourceInfo.none

Instances For

source
def Lean.Syntax.getPos? (stx : Syntax) (canonicalOnly : Bool := false) :
Option String.Pos.Raw

Get the starting position of the syntax, if possible. If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying position information.

Equations

- stx.getPos? canonicalOnly = stx.getHeadInfo.getPos? canonicalOnly

Instances For

source
partial def Lean.Syntax.getTailPos? (stx : Syntax) (canonicalOnly : Bool := false) :
Option String.Pos.Raw

Get the ending position of the syntax, if possible. If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying position information.

source
structure Lean.Syntax.SepArray (sep : String) :
Type

An array of syntax elements interspersed with the given separators.

Separator arrays result from repetition operators such as `,*`. Coercions to and from `Array Syntax` insert or remove separators as required.

The typed equivalent is `Lean.Syntax.TSepArray`.

- elemsAndSeps : Array Syntax

  The array of elements and separators, ordered like `#[el1, sep1, el2, sep2, el3]`.

Instances For

source
structure Lean.Syntax.TSepArray (ks : SyntaxNodeKinds) (sep : String) :
Type

An array of syntax elements that alternate with the given separator. Each syntax element has a kind drawn from `ks`.

Separator arrays result from repetition operators such as `,*`. Coercions to and from `Array (TSyntax ks)` insert or remove separators as required. The untyped equivalent is `Lean.Syntax.SepArray`.

- elemsAndSeps : Array Syntax

  The array of elements and separators, ordered like `#[el1, sep1, el2, sep2, el3]`.

Instances For

source
@[reducible, inline]
abbrev Lean.TSyntaxArray (ks : SyntaxNodeKinds) :
Type

An array of syntaxes of kind `ks`.

Equations

- Lean.TSyntaxArray ks = Array (Lean.TSyntax ks)

Instances For

source
unsafe def Lean.TSyntaxArray.rawImpl {ks : SyntaxNodeKinds} :
TSyntaxArray ks → Array Syntax

Implementation of `TSyntaxArray.raw`.

Equations

- Lean.TSyntaxArray.rawImpl = unsafeCast

Instances For

source
@[implemented_by Lean.TSyntaxArray.rawImpl]
opaque Lean.TSyntaxArray.raw {ks : SyntaxNodeKinds} (as : TSyntaxArray ks) :
Array Syntax

Converts a `TSyntaxArray` to an `Array Syntax`, without reallocation.

source
unsafe def Lean.TSyntaxArray.mkImpl {ks : SyntaxNodeKinds} :
Array Syntax → TSyntaxArray ks

Implementation of `TSyntaxArray.mk`.

Equations

- Lean.TSyntaxArray.mkImpl = unsafeCast

Instances For

source
@[implemented_by Lean.TSyntaxArray.mkImpl]
opaque Lean.TSyntaxArray.mk {ks : SyntaxNodeKinds} (as : Array Syntax) :
TSyntaxArray ks

Converts an `Array Syntax` to a `TSyntaxArray`, without reallocation.

source
def Lean.SourceInfo.fromRef (ref : Syntax) (canonical : Bool := false) :
SourceInfo

Constructs a synthetic `SourceInfo` using a `ref : Syntax` for the span.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.mkAtom (val : String) :
Syntax

Constructs a synthetic `atom` with no source info.

Equations

- Lean.mkAtom val = Lean.Syntax.atom Lean.SourceInfo.none val

Instances For

source
def Lean.mkAtomFrom (src : Syntax) (val : String) (canonical : Bool := false) :
Syntax

Constructs a synthetic `atom` with source info coming from `src`.

Equations

- Lean.mkAtomFrom src val canonical = Lean.Syntax.atom (Lean.SourceInfo.fromRef src canonical) val

Instances For

# Parser descriptions #

source
inductive Lean.ParserDescr :
Type

A `ParserDescr` is a grammar for parsers. This is used by the `syntax` command to produce parsers without having to `import Lean`.

- const (name : Name) : ParserDescr

  A (named) nullary parser, like `ppSpace`

- unary (name : Name) (p : ParserDescr) : ParserDescr

  A (named) unary parser, like `group(p)`

- binary (name : Name) (p₁ p₂ : ParserDescr) : ParserDescr

  A (named) binary parser, like `orelse` or `andthen` (written as `p1 <|> p2` and `p1 p2` respectively in `syntax`)

- node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr) : ParserDescr

  Parses using `p`, then pops the stack to create a new node with kind `kind`. The precedence `prec` is used to determine whether the parser should apply given the current precedence level.

- trailingNode (kind : SyntaxNodeKind) (prec lhsPrec : Nat) (p : ParserDescr) : ParserDescr

  Like `node` but for trailing parsers (which start with a nonterminal). Assumes the lhs is already on the stack, and parses using `p`, then pops the stack including the lhs to create a new node with kind `kind`. The precedence `prec` and `lhsPrec` are used to determine whether the parser should apply.

- symbol (val : String) : ParserDescr

  Parses the literal symbol.

  The symbol is automatically included in the set of reserved tokens ("keywords"). Keywords cannot be used as identifiers, unless the identifier is otherwise escaped. For example, `"fun"` reserves `fun` as a keyword; to refer an identifier named `fun` one can write `«fun»`. Adding a `&` prefix prevents it from being reserved, for example `&"true"`.

  Whitespace before or after the atom is used as a pretty printing hint. For example, `" + "` parses `+` and pretty prints it with whitespace on both sides. The whitespace has no effect on parsing behavior.

- nonReservedSymbol (val : String) (includeIdent : Bool) : ParserDescr

  Parses a literal symbol. The `&` prefix prevents it from being included in the set of reserved tokens ("keywords"). This means that the symbol can still be recognized as an identifier by other parsers.

  Some syntax categories, such as `tactic`, automatically apply `&` to the first symbol.

  Whitespace before or after the atom is used as a pretty printing hint. For example, `" + "` parses `+` and pretty prints it with whitespace on both sides. The whitespace has no effect on parsing behavior.

  (Not exposed by parser description syntax: If the `includeIdent` argument is true, lets `ident` be reinterpreted as `atom` if it matches.)

- cat (catName : Name) (rbp : Nat) : ParserDescr

  Parses using the category parser `catName` with right binding power (i.e. precedence) `rbp`.

- parser (declName : Name) : ParserDescr

  Parses using another parser `declName`, which can be either a `Parser` or `ParserDescr`.

- nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr) : ParserDescr

  Like `node`, but also declares that the body can be matched using an antiquotation with name `name`. For example, `def $id:declId := 1` uses an antiquotation with name `declId` in the place where a `declId` is expected.

- sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) : ParserDescr

  A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`. `psep` is usually the same as `symbol sep`, but it can be overridden. `sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`. `allowTrailingSep` is true if e.g. `a, b,` is also allowed to match.

- sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) : ParserDescr

  `sepBy1` is just like `sepBy`, except it takes 1 or more instead of 0 or more occurrences of `p`.

- unicodeSymbol (val asciiVal : String) (preserveForPP : Bool) : ParserDescr
  - `unicode("→", "->")` parses a symbol matching either `→` or `->`. Each symbol is reserved. The second symbol is an ASCII version of the first. The `pp.unicode` option controls which is used when pretty printing.
  - `unicode("→", "->", preserveForPP)` is the same except for pretty printing behavior. When the `pp.unicode` option is enabled, then the pretty printer uses whichever symbol matches the underlying atom in the syntax. The intent is that `preserveForPP` means that the ASCII variant is preferred. For example, `fun` notation uses `preserveForPP` for its arrow; the delaborator chooses `↦` or `=>` depending on the value of `pp.unicode.fun`, letting users opt-in to formatting with `↦`. Note that `notation` creates a pretty printer preferring the ASCII version.

Instances For

source
instance Lean.instInhabitedParserDescr :
Inhabited ParserDescr
Equations

- Lean.instInhabitedParserDescr = { default := Lean.ParserDescr.symbol "" }

source
@[reducible, inline]
abbrev Lean.TrailingParserDescr :
Type

Although `TrailingParserDescr` is an abbreviation for `ParserDescr`, Lean will look at the declared type in order to determine whether to add the parser to the leading or trailing parser table. The determination is done automatically by the `syntax` command.

Equations

- Lean.TrailingParserDescr = Lean.ParserDescr

Instances For

Runtime support for making quotation terms auto-hygienic, by mangling identifiers introduced by them with a "macro scope" supplied by the context. Details to appear in a paper soon.

source
@[reducible, inline]
abbrev Lean.MacroScope :
Type

A macro scope identifier is just a `Nat` that gets bumped every time we enter a new macro scope. Within a macro scope, all occurrences of identifier `x` parse to the same thing, but `x` parsed from different macro scopes will produce different identifiers.

Equations

- Lean.MacroScope = Nat

Instances For

source
def Lean.reservedMacroScope :
Nat

Macro scope used internally. It is not available for our frontend.

Equations

- Lean.reservedMacroScope = 0

Instances For

source
def Lean.firstFrontendMacroScope :
Nat

First macro scope available for our frontend

Equations

- Lean.firstFrontendMacroScope = Lean.reservedMacroScope + 1

Instances For

source
class Lean.MonadRef (m : Type → Type) :
Type 1

A `MonadRef` is a monad that has a `ref : Syntax` in the read-only state. This is used to keep track of the location where we are working; if an exception is thrown, the `ref` gives the location where the error will be reported, assuming no more specific location is provided.

- getRef : m Syntax

  Get the current value of the `ref`

- withRef {α : Type} : Syntax → m α → m α

  Run `x : m α` with a modified value for the `ref`

Instances

source
instance Lean.instMonadRefOfMonadLiftOfMonadFunctor (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadRef m] :
MonadRef n
Equations

- One or more equations did not get rendered due to their size.

source
def Lean.replaceRef (ref oldRef : Syntax) :
Syntax

Replaces `oldRef` with `ref`, unless `ref` has no position info. This biases us to having a valid span to report an error on.

Equations

- Lean.replaceRef ref oldRef = match ref.getPos? with | some val => ref | x => oldRef

Instances For

source
@[inline]
def Lean.withRef {m : Type → Type} [Monad m] [MonadRef m] {α : Type} (ref : Syntax) (x : m α) :
m α

Run `x : m α` with a modified value for the `ref`. This is not exactly the same as `MonadRef.withRef`, because it uses `replaceRef` to avoid putting syntax with bad spans in the state.

Equations

- Lean.withRef ref x = do let oldRef ← Lean.getRef have ref : Lean.Syntax := Lean.replaceRef ref oldRef Lean.MonadRef.withRef ref x

Instances For

source
@[inline]
def Lean.withRef? {m : Type → Type} [Monad m] [MonadRef m] {α : Type} (ref? : Option Syntax) (x : m α) :
m α

If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`. Otherwise, run `x` directly.

Equations

- Lean.withRef? (some ref) x = Lean.withRef ref x
- Lean.withRef? ref? x = x

Instances For

source
class Lean.MonadQuotation (m : Type → Type) extends Lean.MonadRef m :
Type 1

A monad that supports syntax quotations. Syntax quotations (in term position) are monadic values that when executed retrieve the current "macro scope" from the monad and apply it to every identifier they introduce (independent of whether this identifier turns out to be a reference to an existing declaration, or an actually fresh binding during further elaboration). We also apply the position of the result of `getRef` to each introduced symbol, which results in better error positions than not applying any position.

- getRef : m Syntax
- withRef {α : Type} : Syntax → m α → m α
- getCurrMacroScope : m MacroScope

  Get the fresh scope of the current macro invocation

- getContext : m Name

  Get the context name used in Note `Macro Scope Representation`.

- withFreshMacroScope {α : Type} : m α → m α

  Execute action in a new macro invocation context. This transformer should be used at all places that morally qualify as the beginning of a "macro call", e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it can also be used internally inside a "macro" if identifiers introduced by e.g. different recursive calls should be independent and not collide. While returning an intermediate syntax tree that will recursively be expanded by the elaborator can be used for the same effect, doing direct recursion inside the macro guarded by this transformer is often easier because one is not restricted to passing a single syntax tree. Modelling this helper as a transformer and not just a monadic action ensures that the current macro scope before the recursive call is restored after it, as expected.

Instances

source
@[reducible, inline]
abbrev Lean.MonadQuotation.getMainModule {m : Type → Type} [self : MonadQuotation m] :
m Name

Get the context name used in Note `Macro Scope Representation`.

Equations

- @Lean.MonadQuotation.getMainModule = @Lean.MonadQuotation.getContext

Instances For

source
@[inline]
def Lean.MonadRef.mkInfoFromRefPos {m : Type → Type} [Monad m] [MonadRef m] :
m SourceInfo

Construct a synthetic `SourceInfo` from the `ref` in the monad state.

Equations

- Lean.MonadRef.mkInfoFromRefPos = do let __do_lift ← Lean.getRef pure (Lean.SourceInfo.fromRef __do_lift)

Instances For

source
instance Lean.instMonadQuotationOfMonadFunctorOfMonadLift {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] :
MonadQuotation n
Equations

- One or more equations did not get rendered due to their size.

# Note [Macro Scope Representation] #

We represent a name with macro scopes as

    <actual name>._@.(<ctx>.<scopes>)*.<ctx>._hyg.<scopes>

Example: suppose the context name is `Init.Data.List.Basic`, and name is `foo.bla`, and macroscopes [2, 5]

    foo.bla._@.Init.Data.List.Basic._hyg.2.5

The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.

The primary purpose of the context name is to differentiate macro scopes from different files as the numeric scopes are reset in each file. The current scope is always the right-most one. Scopes from multiple files may be collected when we execute a macro generated in an imported file in the current file.

    foo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4

The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance. In practice, we further specify the context name down to be unique per declaration so that the numeric scopes are not influenced by the elaboration of preceding declarations. This helps both with ensuring declaration names are more stable so that `prefer_native` can find the correct native symbol as well as making exported information in general more stable, avoiding rebuilds under the module system. Thus the actual encoding of the context name in the current implementation is

    <main module>.<uniq>._hygCtx

where `<uniq>` is an identifier unique within the current module, set by `Command.withInitQuotContext`; see there for details. Thus we can assume the full context name to be unique throughout all modules and reset the numeric scopes whenever establishing a fresh context name.

source
def Lean.Name.hasMacroScopes :
Name → Bool

Does this name have hygienic macro scopes?

Equations

- (pre.str s).hasMacroScopes = (s == "_hyg")
- (p.num i).hasMacroScopes = p.hasMacroScopes
- x✝.hasMacroScopes = false

Instances For

source
@[export lean_erase_macro_scopes]
def Lean.Name.eraseMacroScopes (n : Name) :
Name

Remove the macro scopes from the name.

Equations

- n.eraseMacroScopes = match n.hasMacroScopes with | true => Lean.eraseMacroScopesAux✝ n | false => n

Instances For

source
@[export lean_simp_macro_scopes]
def Lean.Name.simpMacroScopes (n : Name) :
Name

Helper function we use to create binder names that do not need to be unique.

Equations

- n.simpMacroScopes = match n.hasMacroScopes with | true => Lean.simpMacroScopesAux✝ n | false => n

Instances For

source
structure Lean.MacroScopesView :
Type

A `MacroScopesView` represents a parsed hygienic name. `extractMacroScopes` will decode it from a `Name`, and `.review` will re-encode it. The grammar of a hygienic name is:

    <name>._@.(<module_name>.<scopes>)*.<mainModule>._hyg.<scopes>

- name : Name

  The original (unhygienic) name.

- imported : Name

  All the name components `(<module_name>.<scopes>)*` from the imports concatenated together.

- ctx : Name

  The context name, a globally unique prefix.

- scopes : List MacroScope

  The list of macro scopes.

Instances For

source
instance Lean.instInhabitedMacroScopesView :
Inhabited MacroScopesView
Equations

- Lean.instInhabitedMacroScopesView = { default := { name := default, imported := default, ctx := default, scopes := default } }

source
def Lean.MacroScopesView.review (view : MacroScopesView) :
Name

Encode a hygienic name from the parsed pieces.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.extractMacroScopes (n : Name) :
MacroScopesView

Revert all `addMacroScope` calls. `v = extractMacroScopes n → n = v.review`. This operation is useful for analyzing/transforming the original identifiers, then adding back the scopes (via `MacroScopesView.review`).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.addMacroScope (ctx n : Name) (scp : MacroScope) :
Name

Add a new macro scope onto the name `n`, in the given `ctx`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Name.append (a b : Name) :
Name

Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result. Panics if both `a` and `b` have macro scopes.

This function is used for the `Append Name` instance.

See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes. Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instAppendName :
Append Name
Equations

- Lean.instAppendName = { append := Lean.Name.append }

source
@[inline]
def Lean.MonadQuotation.addMacroScope {m : Type → Type} [MonadQuotation m] [Monad m] (n : Name) :
m Name

Add a new macro scope onto the name `n`, using the monad state to supply the main module and current macro scope.

Equations

- Lean.MonadQuotation.addMacroScope n = do let ctx ← Lean.MonadQuotation.getContext let scp ← Lean.getCurrMacroScope pure (Lean.addMacroScope ctx n scp)

Instances For

source
def Lean.Syntax.matchesNull (stx : Syntax) (n : Nat) :
Bool

Is this syntax a null `node`?

Equations

- stx.matchesNull n = stx.isNodeOf Lean.nullKind n

Instances For

source
def Lean.Syntax.matchesIdent (stx : Syntax) (id : Name) :
Bool

Function used for determining whether a syntax pattern ``(id)` is matched. There are various conceivable notions of when two syntactic identifiers should be regarded as identical, but semantic definitions like whether they refer to the same global name cannot be implemented without context information (i.e. `MonadResolveName`). Thus in patterns we default to the structural solution of comparing the identifiers' `Name` values, though we at least do so modulo macro scopes so that identifiers that "look" the same match. This is particularly useful when dealing with identifiers that do not actually refer to Lean bindings, e.g. in the `stx` pattern ``(many($p))`.

Equations

- stx.matchesIdent id = (stx.isIdent && stx.getId.eraseMacroScopes == id.eraseMacroScopes)

Instances For

source
def Lean.Syntax.matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) :
Bool

Is this syntax a node kind `k` wrapping an `atom _ val`?

Equations

- (Lean.Syntax.node info kind args).matchesLit k val = (k == kind && match args.getD 0 Lean.Syntax.missing with | Lean.Syntax.atom info val' => val == val' | x => false)
- stx.matchesLit k val = false

Instances For

source
opaque Lean.Macro.MethodsRefPointed :
NonemptyType

References

source
def Lean.Macro.MethodsRef :
Type
Equations

- Lean.Macro.MethodsRef = Lean.Macro.MethodsRefPointed.type

Instances For

source
instance Lean.Macro.instNonemptyMethodsRef :
Nonempty MethodsRef
source
structure Lean.Macro.Context :
Type

The read-only context for the `MacroM` monad.

- methods : MethodsRef

  An opaque reference to the `Methods` object. This is done to break a dependency cycle: the `Methods` involve `MacroM` which has not been defined yet.

- quotContext : Name

  The quotation context name for `MonadQuotation.getContext`.

- currMacroScope : MacroScope

  The current macro scope.

- currRecDepth : Nat

  The current recursion depth.

- maxRecDepth : Nat

  The maximum recursion depth.

- ref : Syntax

  The syntax which supplies the position of error messages.

Instances For

source
inductive Lean.Macro.Exception :
Type

An exception in the `MacroM` monad.

- error : Syntax → String → Exception

  A general error, given a message and a span (expressed as a `Syntax`).

- unsupportedSyntax : Exception

  An unsupported syntax exception. We keep this separate because it is used for control flow: if one macro does not support a syntax then we try the next one.

Instances For

source
structure Lean.Macro.State :
Type

The mutable state for the `MacroM` monad.

- macroScope : MacroScope

  The global macro scope counter, used for producing fresh scope names.

- traceMsgs : List (Name × String)

  The list of trace messages that have been produced, each with a trace class and a message.

- expandedMacroDecls : List Lean.Name

Instances For

source
instance Lean.Macro.instInhabitedState :
Inhabited State
Equations

- Lean.Macro.instInhabitedState = { default := Lean.Macro.instInhabitedState.default }

source
def Lean.Macro.instInhabitedState.default :
State
Equations

- Lean.Macro.instInhabitedState.default = { macroScope := default, traceMsgs := default, expandedMacroDecls := default }

Instances For

source
@[reducible, inline]
abbrev Lean.MacroM (α : Type) :
Type

The `MacroM` monad is the main monad for macro expansion. It has the information needed to handle hygienic name generation, and is the monad that `macro` definitions live in.

Notably, this is a (relatively) pure monad: there is no `IO` and no access to the `Environment`. That means that things like declaration lookup are impossible here, as well as `IO.Ref` or other side-effecting operations. For more capabilities, macros can instead be written as `elab` using `adaptExpander`.

Equations

- Lean.MacroM = ReaderT Lean.Macro.Context (EStateM Lean.Macro.Exception Lean.Macro.State)

Instances For

source
@[reducible, inline]
abbrev Lean.Macro :
Type

A `macro` has type `Macro`, which is a `Syntax → MacroM Syntax`: it receives an input syntax and is supposed to "expand" it into another piece of syntax.

Equations

- Lean.Macro = (Lean.Syntax → Lean.MacroM Lean.Syntax)

Instances For

source
instance Lean.Macro.instMonadRefMacroM :
MonadRef MacroM
Equations

- One or more equations did not get rendered due to their size.

source
def Lean.Macro.throwUnsupported {α : Type} :
MacroM α

Throw an `unsupportedSyntax` exception.

Equations

- Lean.Macro.throwUnsupported = throw Lean.Macro.Exception.unsupportedSyntax

Instances For

source
def Lean.Macro.throwError {α : Type} (msg : String) :
MacroM α

Throw an error with the given message, using the `ref` for the location information.

Equations

- Lean.Macro.throwError msg = do let ref ← Lean.getRef throw (Lean.Macro.Exception.error ref msg)

Instances For

source
def Lean.Macro.throwErrorAt {α : Type} (ref : Syntax) (msg : String) :
MacroM α

Throw an error with the given message and location information.

Equations

- Lean.Macro.throwErrorAt ref msg = Lean.withRef ref (Lean.Macro.throwError msg)

Instances For

source
@[inline]
def Lean.Macro.withFreshMacroScope {α : Type} (x : MacroM α) :
MacroM α

Increments the macro scope counter so that inside the body of `x` the macro scope is fresh.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def Lean.Macro.withIncRecDepth {α : Type} (ref : Syntax) (x : MacroM α) :
MacroM α

Run `x` with an incremented recursion depth counter.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.Macro.instMonadQuotationMacroM :
MonadQuotation MacroM
Equations

- One or more equations did not get rendered due to their size.

source
def Lean.Macro.addMacroScope (n : Name) :
MacroM Name

Add a new macro scope to the name `n`.

Equations

- Lean.Macro.addMacroScope n = Lean.MonadQuotation.addMacroScope n

Instances For

source
structure Lean.Macro.Methods :
Type

The opaque methods that are available to `MacroM`.

- expandMacro? : Syntax → MacroM (Option Syntax)

  Expands macros in the given syntax. A return value of `none` means there was nothing to expand.

- getCurrNamespace : MacroM Name

  Get the current namespace in the file.

- hasDecl : Name → MacroM Bool

  Check if a given name refers to a declaration.

- resolveNamespace : Name → MacroM (List Name)

  Resolves the given name to an overload list of namespaces.

- resolveGlobalName : Name → MacroM (List (Name × List String))

  Resolves the given name to an overload list of global definitions. The `List String` in each alternative is the deduced list of projections (which are ambiguous with name components).

Instances For

source
def Lean.Macro.instInhabitedMethods.default :
Methods
Equations

- Lean.Macro.instInhabitedMethods.default = { expandMacro? := default, getCurrNamespace := default, hasDecl := default, resolveNamespace := default, resolveGlobalName := default }

Instances For

source
instance Lean.Macro.instInhabitedMethods :
Inhabited Methods
Equations

- Lean.Macro.instInhabitedMethods = { default := Lean.Macro.instInhabitedMethods.default }

source
unsafe def Lean.Macro.mkMethodsImp (methods : Methods) :
MethodsRef

Implementation of `mkMethods`.

Equations

- Lean.Macro.mkMethodsImp methods = unsafeCast methods

Instances For

source
@[implemented_by Lean.Macro.mkMethodsImp]
opaque Lean.Macro.mkMethods (methods : Methods) :
MethodsRef

Make an opaque reference to a `Methods`.

source
instance Lean.Macro.instInhabitedMethodsRef :
Inhabited MethodsRef
Equations

- Lean.Macro.instInhabitedMethodsRef = { default := Lean.Macro.mkMethods default }

source
unsafe def Lean.Macro.getMethodsImp :
MacroM Methods

Implementation of `getMethods`.

Equations

- Lean.Macro.getMethodsImp = do let ctx ← read pure (unsafeCast ctx.methods)

Instances For

source
@[implemented_by Lean.Macro.getMethodsImp]
opaque Lean.Macro.getMethods :
MacroM Methods

Extract the methods list from the `MacroM` state.

source
def Lean.Macro.expandMacro? (stx : Syntax) :
MacroM (Option Syntax)

`expandMacro? stx` returns `some stxNew` if `stx` is a macro, and `stxNew` is its expansion.

Equations

- Lean.expandMacro? stx = do let __do_lift ← Lean.Macro.getMethods __do_lift.expandMacro? stx

Instances For

source
def Lean.Macro.hasDecl (declName : Name) :
MacroM Bool

Returns `true` if the environment contains a declaration with name `declName`

Equations

- Lean.Macro.hasDecl declName = do let __do_lift ← Lean.Macro.getMethods __do_lift.hasDecl declName

Instances For

source
def Lean.Macro.getCurrNamespace :
MacroM Name

Gets the current namespace given the position in the file.

Equations

- Lean.Macro.getCurrNamespace = do let __do_lift ← Lean.Macro.getMethods __do_lift.getCurrNamespace

Instances For

source
def Lean.Macro.resolveNamespace (n : Name) :
MacroM (List Name)

Resolves the given name to an overload list of namespaces.

Equations

- Lean.Macro.resolveNamespace n = do let __do_lift ← Lean.Macro.getMethods __do_lift.resolveNamespace n

Instances For

source
def Lean.Macro.resolveGlobalName (n : Name) :
MacroM (List (Name × List String))

Resolves the given name to an overload list of global definitions. The `List String` in each alternative is the deduced list of projections (which are ambiguous with name components).

Remark: it will not trigger actions associated with reserved names. Recall that Lean has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem containing stating that `foo` is equal to its definition. The action associated with `foo.def` automatically proves the theorem. At the macro level, the name is resolved, but the action is not executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.

Equations

- Lean.Macro.resolveGlobalName n = do let __do_lift ← Lean.Macro.getMethods __do_lift.resolveGlobalName n

Instances For

source
def Lean.Macro.trace (clsName : Name) (msg : String) :
MacroM Unit

Add a new trace message, with the given trace class and message.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Lean.PrettyPrinter.UnexpandM (α : Type) :
Type

The unexpander monad, essentially `Syntax → Option α`. The `Syntax` is the `ref`, and it has the possibility of failure without an error message.

Equations

- Lean.PrettyPrinter.UnexpandM = ReaderT Lean.Syntax (EStateM Unit Unit)

Instances For

source
@[reducible, inline]
abbrev Lean.PrettyPrinter.Unexpander :
Type

Function that tries to reverse macro expansions as a post-processing step of delaboration. While less general than an arbitrary delaborator, it can be declared without importing `Lean`. Used by the `[app_unexpander]` attribute.

Equations

- Lean.PrettyPrinter.Unexpander = (Lean.Syntax → Lean.PrettyPrinter.UnexpandM Lean.Syntax)

Instances For

source
instance Lean.PrettyPrinter.instMonadQuotationUnexpandM :
MonadQuotation UnexpandM
Equations

- One or more equations did not get rendered due to their size.