Documentation

Init.Core

def inline {α : Sort u} (a : α) :
α

inline (f x) is an indication to the compiler to inline the definition of f at the application site itself (by comparison to the @[inline] attribute, which applies to all applications of the function).

Equations
Instances For
    theorem id_def {α : Sort u} (a : α) :
    id a = a
    @[inline]
    def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : αβφ) :
    βαφ

    flip f a b is f b a. It is useful for "point-free" programming, since it can sometimes be used to avoid introducing variables. For example, (·<·) is the less-than relation, and flip (·<·) is the greater-than relation.

    Equations
    Instances For
      @[simp]
      theorem Function.const_apply {β : Sort u_1} {α : Sort u_2} {y : β} {x : α} :
      Function.const α y x = y
      @[simp]
      theorem Function.comp_apply {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : βδ} {g : αβ} {x : α} :
      (f g) x = f (g x)
      theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : βδ) (g : αβ) :
      f g = fun (x : α) => f (g x)
      @[simp]
      theorem Function.const_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {c : γ} :
      @[simp]
      theorem Function.comp_const {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} {f : βγ} {b : β} :
      @[simp]
      theorem Function.true_comp {α : Sort u_1} {β : Sort u_2} {f : αβ} :
      (fun (x : β) => true) f = fun (x : α) => true
      @[simp]
      theorem Function.false_comp {α : Sort u_1} {β : Sort u_2} {f : αβ} :
      (fun (x : β) => false) f = fun (x : α) => false
      @[macro_inline]
      def Empty.elim {C : Sort u} :
      EmptyC

      Empty.elim : Empty → C says that a value of any type can be constructed from Empty. This can be thought of as a compiler-checked assertion that a code path is unreachable.

      This is a non-dependent variant of Empty.rec.

      Equations
      Instances For

        Decidable equality for Empty

        Equations
        @[macro_inline]
        def PEmpty.elim {C : Sort u_1} :
        PEmptyC

        PEmpty.elim : Empty → C says that a value of any type can be constructed from PEmpty. This can be thought of as a compiler-checked assertion that a code path is unreachable.

        This is a non-dependent variant of PEmpty.rec.

        Equations
          Instances For

            Decidable equality for PEmpty

            Equations
            structure Thunk (α : Type u) :

            Thunks are "lazy" values that are evaluated when first accessed using Thunk.get/map/bind. The value is then stored and not recomputed for all further accesses.

            Instances For
              @[extern lean_thunk_pure]
              def Thunk.pure {α : Type u_1} (a : α) :

              Store a value in a thunk. Note that the value has already been computed, so there is no laziness.

              Equations
              Instances For
                @[extern lean_thunk_get_own]
                def Thunk.get {α : Type u_1} (x : Thunk α) :
                α

                Forces a thunk to extract the value. This will cache the result, so a second call to the same function will return the value in O(1) instead of calling the stored getter function.

                Equations
                Instances For
                  @[inline]
                  def Thunk.map {α : Type u_1} {β : Type u_2} (f : αβ) (x : Thunk α) :

                  Map a function over a thunk.

                  Equations
                  Instances For
                    @[inline]
                    def Thunk.bind {α : Type u_1} {β : Type u_2} (x : Thunk α) (f : αThunk β) :

                    Constructs a thunk that applies f to the result of x when forced.

                    Equations
                    • x.bind f = { fn := fun (x_1 : Unit) => (f x.get).get }
                    Instances For
                      @[simp]
                      theorem Thunk.sizeOf_eq {α : Type u_1} [SizeOf α] (a : Thunk α) :
                      sizeOf a = 1 + sizeOf a.get
                      instance thunkCoe {α : Type u_1} :
                      CoeTail α (Thunk α)
                      Equations
                      • thunkCoe = { coe := fun (a : α) => { fn := fun (x : Unit) => a } }

                      definitions #

                      structure Iff (a : Prop) (b : Prop) :

                      If and only if, or logical bi-implication. a ↔ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

                      • intro :: (
                        • mp : ab

                          Modus ponens for if and only if. If a ↔ b and a, then b.

                        • mpr : ba

                          Modus ponens for if and only if, reversed. If a ↔ b and b, then a.

                      • )
                      Instances For
                        theorem Iff.mp {a : Prop} {b : Prop} (self : a b) :
                        ab

                        Modus ponens for if and only if. If a ↔ b and a, then b.

                        theorem Iff.mpr {a : Prop} {b : Prop} (self : a b) :
                        ba

                        Modus ponens for if and only if, reversed. If a ↔ b and b, then a.

                        If and only if, or logical bi-implication. a ↔ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

                        Equations
                        Instances For

                          If and only if, or logical bi-implication. a ↔ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

                          Equations
                          Instances For
                            inductive Sum (α : Type u) (β : Type v) :
                            Type (max u v)

                            Sum α β, or α ⊕ β, is the disjoint union of types α and β. An element of α ⊕ β is either of the form .inl a where a : α, or .inr b where b : β.

                            • inl: {α : Type u} → {β : Type v} → αα β

                              Left injection into the sum type α ⊕ β. If a : α then .inl a : α ⊕ β.

                            • inr: {α : Type u} → {β : Type v} → βα β

                              Right injection into the sum type α ⊕ β. If b : β then .inr b : α ⊕ β.

                            Instances For

                              Sum α β, or α ⊕ β, is the disjoint union of types α and β. An element of α ⊕ β is either of the form .inl a where a : α, or .inr b where b : β.

                              Equations
                              Instances For
                                inductive PSum (α : Sort u) (β : Sort v) :
                                Sort (max (max 1 u) v)

                                PSum α β, or α ⊕' β, is the disjoint union of types α and β. It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat.

                                The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSum is usually only used in automation that constructs sums of arbitrary types.

                                • inl: {α : Sort u} → {β : Sort v} → αα ⊕' β

                                  Left injection into the sum type α ⊕' β. If a : α then .inl a : α ⊕' β.

                                • inr: {α : Sort u} → {β : Sort v} → βα ⊕' β

                                  Right injection into the sum type α ⊕' β. If b : β then .inr b : α ⊕' β.

                                Instances For

                                  PSum α β, or α ⊕' β, is the disjoint union of types α and β. It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat.

                                  The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSum is usually only used in automation that constructs sums of arbitrary types.

                                  Equations
                                  Instances For
                                    instance instInhabitedPSum {α : Sort u_1} {β : Sort u_2} [Inhabited α] :
                                    Inhabited (α ⊕' β)
                                    Equations
                                    • instInhabitedPSum = { default := PSum.inl default }
                                    instance instInhabitedPSum_1 {α : Sort u_1} {β : Sort u_2} [Inhabited β] :
                                    Inhabited (α ⊕' β)
                                    Equations
                                    • instInhabitedPSum_1 = { default := PSum.inr default }
                                    @[unbox]
                                    structure Sigma {α : Type u} (β : αType v) :
                                    Type (max u v)

                                    Sigma β, also denoted Σ a : α, β a or (a : α) × β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It is sometimes known as the dependent sum type, since it is the type level version of an indexed summation.

                                    • fst : α

                                      The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

                                    • snd : β self.fst

                                      The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.

                                    Instances For
                                      structure PSigma {α : Sort u} (β : αSort v) :
                                      Sort (max (max 1 u) v)

                                      PSigma β, also denoted Σ' a : α, β a or (a : α) ×' β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It differs from Σ a : α, β a in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like (p : Nat) ×' p = p.

                                      The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSigma is usually only used in automation that constructs pairs of arbitrary types.

                                      • fst : α

                                        The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

                                      • snd : β self.fst

                                        The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.

                                      Instances For
                                        inductive Exists {α : Sort u} (p : αProp) :

                                        Existential quantification. If p : α → Prop is a predicate, then ∃ x : α, p x asserts that there is some x of type α such that p x holds. To create an existential proof, use the exists tactic, or the anonymous constructor notation ⟨x, h⟩. To unpack an existential, use cases h where h is a proof of ∃ x : α, p x, or let ⟨x, hx⟩ := h where `.

                                        Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:

                                        example (h : ∃ x : Nat, x = x) : Nat :=
                                          let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
                                          x
                                        

                                        The error message recursor 'Exists.casesOn' can only eliminate into Prop means that this only works when the current goal is another proposition:

                                        example (h : ∃ x : Nat, x = x) : True :=
                                          let ⟨x, _⟩ := h  -- ok, because the goal is `True : Prop`
                                          trivial
                                        
                                        • intro: ∀ {α : Sort u} {p : αProp} (w : α), p wExists p

                                          Existential introduction. If a : α and h : p a, then ⟨a, h⟩ is a proof that ∃ x : α, p x.

                                        Instances For
                                          inductive ForInStep (α : Type u) :

                                          Auxiliary type used to compile for x in xs notation.

                                          This is the return value of the body of a ForIn call, representing the body of a for loop. It can be:

                                          • .yield (a : α), meaning that we should continue the loop and a is the new state. .yield is produced by continue and reaching the bottom of the loop body.
                                          • .done (a : α), meaning that we should early-exit the loop with state a. .done is produced by calls to break or return in the loop,
                                          • done: {α : Type u} → αForInStep α

                                            .done a means that we should early-exit the loop. .done is produced by calls to break or return in the loop.

                                          • yield: {α : Type u} → αForInStep α

                                            .yield a means that we should continue the loop. .yield is produced by continue and reaching the bottom of the loop body.

                                          Instances For
                                            instance instInhabitedForInStep :
                                            {a : Type u_1} → [inst : Inhabited a] → Inhabited (ForInStep a)
                                            Equations
                                            class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) :
                                            Type (max (max (max u (u₁ + 1)) u₂) v)

                                            ForIn m ρ α is the typeclass which supports for x in xs notation. Here xs : ρ is the type of the collection to iterate over, x : α is the element type which is made available inside the loop, and m is the monad for the encompassing do block.

                                            • forIn : {β : Type u₁} → [inst : Monad m] → ρβ(αβm (ForInStep β))m β

                                              forIn x b f : m β runs a for-loop in the monad m with additional state β. This traverses over the "contents" of x, and passes the elements a : α to f : α → β → m (ForInStep β). b : β is the initial state, and the return value of f is the new state as well as a directive .done or .yield which indicates whether to abort early or continue iteration.

                                              The expression

                                              let mut b := ...
                                              for x in xs do
                                                b ← foo x b
                                              

                                              in a do block is syntactic sugar for:

                                              let b := ...
                                              let b ← forIn xs b (fun x b => do
                                                let b ← foo x b
                                                return .yield b)
                                              

                                              (Here b corresponds to the variables mutated in the loop.)

                                            Instances
                                              class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) :
                                              Type (max (max (max u (u₁ + 1)) u₂) v)

                                              ForIn' m ρ α d is a variation on the ForIn m ρ α typeclass which supports the for h : x in xs notation. It is the same as for x in xs except that h : x ∈ xs is provided as an additional argument to the body of the for-loop.

                                              • forIn' : {β : Type u₁} → [inst : Monad m] → (x : ρ) → β((a : α) → a xβm (ForInStep β))m β

                                                forIn' x b f : m β runs a for-loop in the monad m with additional state β. This traverses over the "contents" of x, and passes the elements a : α along with a proof that a ∈ x to f : (a : α) → a ∈ x → β → m (ForInStep β). b : β is the initial state, and the return value of f is the new state as well as a directive .done or .yield which indicates whether to abort early or continue iteration.

                                              Instances
                                                inductive DoResultPRBC (α : Type u) (β : Type u) (σ : Type u) :

                                                Auxiliary type used to compile do notation. It is used when compiling a do block nested inside a combinator like tryCatch. It encodes the possible ways the block can exit:

                                                • pure (a : α) s means that the block exited normally with return value a.
                                                • return (b : β) s means that the block exited via a return b early-exit command.
                                                • break s means that break was called, meaning that we should exit from the containing loop.
                                                • continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop.

                                                All cases return a value s : σ which bundles all the mutable variables of the do-block.

                                                • pure: {α β σ : Type u} → ασDoResultPRBC α β σ

                                                  pure (a : α) s means that the block exited normally with return value a

                                                • return: {α β σ : Type u} → βσDoResultPRBC α β σ

                                                  return (b : β) s means that the block exited via a return b early-exit command

                                                • break: {α β σ : Type u} → σDoResultPRBC α β σ

                                                  break s means that break was called, meaning that we should exit from the containing loop

                                                • continue: {α β σ : Type u} → σDoResultPRBC α β σ

                                                  continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

                                                Instances For
                                                  inductive DoResultPR (α : Type u) (β : Type u) (σ : Type u) :

                                                  Auxiliary type used to compile do notation. It is the same as DoResultPRBC α β σ except that break and continue are not available because we are not in a loop context.

                                                  • pure: {α β σ : Type u} → ασDoResultPR α β σ

                                                    pure (a : α) s means that the block exited normally with return value a

                                                  • return: {α β σ : Type u} → βσDoResultPR α β σ

                                                    return (b : β) s means that the block exited via a return b early-exit command

                                                  Instances For
                                                    inductive DoResultBC (σ : Type u) :

                                                    Auxiliary type used to compile do notation. It is an optimization of DoResultPRBC PEmpty PEmpty σ to remove the impossible cases, used when neither pure nor return are possible exit paths.

                                                    • break: {σ : Type u} → σDoResultBC σ

                                                      break s means that break was called, meaning that we should exit from the containing loop

                                                    • continue: {σ : Type u} → σDoResultBC σ

                                                      continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

                                                    Instances For
                                                      inductive DoResultSBC (α : Type u) (σ : Type u) :

                                                      Auxiliary type used to compile do notation. It is an optimization of either DoResultPRBC α PEmpty σ or DoResultPRBC PEmpty α σ to remove the impossible case, used when either pure or return is never used.

                                                      • pureReturn: {α σ : Type u} → ασDoResultSBC α σ

                                                        This encodes either pure (a : α) or return (a : α):

                                                        • pure (a : α) s means that the block exited normally with return value a
                                                        • return (b : β) s means that the block exited via a return b early-exit command

                                                        The one that is actually encoded depends on the context of use.

                                                      • break: {α σ : Type u} → σDoResultSBC α σ

                                                        break s means that break was called, meaning that we should exit from the containing loop

                                                      • continue: {α σ : Type u} → σDoResultSBC α σ

                                                        continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

                                                      Instances For
                                                        class HasEquiv (α : Sort u) :
                                                        Sort (max u (v + 1))

                                                        HasEquiv α is the typeclass which supports the notation x ≈ y where x y : α.

                                                        • Equiv : ααSort v

                                                          x ≈ y says that x and y are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent.

                                                        Instances

                                                          x ≈ y says that x and y are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent.

                                                          Equations
                                                          Instances For

                                                            set notation #

                                                            class HasSubset (α : Type u) :

                                                            Notation type class for the subset relation .

                                                            • Subset : ααProp

                                                              Subset relation: a ⊆ b

                                                            Instances
                                                              class HasSSubset (α : Type u) :

                                                              Notation type class for the strict subset relation .

                                                              • SSubset : ααProp

                                                                Strict subset relation: a ⊂ b

                                                              Instances
                                                                @[reducible, inline]
                                                                abbrev Superset {α : Type u_1} [HasSubset α] (a : α) (b : α) :

                                                                Superset relation: a ⊇ b

                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev SSuperset {α : Type u_1} [HasSSubset α] (a : α) (b : α) :

                                                                  Strict superset relation: a ⊃ b

                                                                  Equations
                                                                  Instances For
                                                                    class Union (α : Type u) :

                                                                    Notation type class for the union operation .

                                                                    • union : ααα

                                                                      a ∪ b is the union ofa and b.

                                                                    Instances
                                                                      class Inter (α : Type u) :

                                                                      Notation type class for the intersection operation .

                                                                      • inter : ααα

                                                                        a ∩ b is the intersection ofa and b.

                                                                      Instances
                                                                        class SDiff (α : Type u) :

                                                                        Notation type class for the set difference \.

                                                                        • sdiff : ααα

                                                                          a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

                                                                        Instances

                                                                          Subset relation: a ⊆ b

                                                                          Equations
                                                                          Instances For

                                                                            Strict subset relation: a ⊂ b

                                                                            Equations
                                                                            Instances For

                                                                              Superset relation: a ⊇ b

                                                                              Equations
                                                                              Instances For

                                                                                Strict superset relation: a ⊃ b

                                                                                Equations
                                                                                Instances For

                                                                                  a ∪ b is the union ofa and b.

                                                                                  Equations
                                                                                  Instances For

                                                                                    a ∩ b is the intersection ofa and b.

                                                                                    Equations
                                                                                    Instances For

                                                                                      a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

                                                                                      Equations
                                                                                      Instances For

                                                                                        collections #

                                                                                        class EmptyCollection (α : Type u) :

                                                                                        EmptyCollection α is the typeclass which supports the notation , also written as {}.

                                                                                        • emptyCollection : α

                                                                                          or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

                                                                                        Instances

                                                                                          or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

                                                                                          Equations
                                                                                          Instances For

                                                                                            or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

                                                                                            Equations
                                                                                            Instances For
                                                                                              class Insert (α : outParam (Type u)) (γ : Type v) :
                                                                                              Type (max u v)

                                                                                              Type class for the insert operation. Used to implement the { a, b, c } syntax.

                                                                                              • insert : αγγ

                                                                                                insert x xs inserts the element x into the collection xs.

                                                                                              Instances
                                                                                                class Singleton (α : outParam (Type u)) (β : Type v) :
                                                                                                Type (max u v)

                                                                                                Type class for the singleton operation. Used to implement the { a, b, c } syntax.

                                                                                                • singleton : αβ

                                                                                                  singleton x is a collection with the single element x (notation: {x}).

                                                                                                Instances
                                                                                                  class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :

                                                                                                  insert x ∅ = {x}

                                                                                                  Instances
                                                                                                    @[simp]
                                                                                                    theorem LawfulSingleton.insert_emptyc_eq {α : Type u} {β : Type v} [EmptyCollection β] [Insert α β] [Singleton α β] [self : LawfulSingleton α β] (x : α) :
                                                                                                    insert x = {x}

                                                                                                    insert x ∅ = {x}

                                                                                                    class Sep (α : outParam (Type u)) (γ : Type v) :
                                                                                                    Type (max u v)

                                                                                                    Type class used to implement the notation { a ∈ c | p a }

                                                                                                    • sep : (αProp)γγ

                                                                                                      Computes { a ∈ c | p a }.

                                                                                                    Instances
                                                                                                      structure Task (α : Type u) :

                                                                                                      Task α is a primitive for asynchronous computation. It represents a computation that will resolve to a value of type α, possibly being computed on another thread. This is similar to Future in Scala, Promise in Javascript, and JoinHandle in Rust.

                                                                                                      The tasks have an overridden representation in the runtime.

                                                                                                      • pure :: (
                                                                                                        • get : α

                                                                                                          If task : Task α then task.get : α blocks the current thread until the value is available, and then returns the result of the task.

                                                                                                      • )
                                                                                                      Instances For
                                                                                                        instance instInhabitedTask :
                                                                                                        {a : Type u_1} → [inst : Inhabited a] → Inhabited (Task a)
                                                                                                        Equations
                                                                                                        • instInhabitedTask = { default := { get := default } }
                                                                                                        instance instNonemptyTask :
                                                                                                        ∀ {α : Type u_1} [inst : Nonempty α], Nonempty (Task α)
                                                                                                        Equations
                                                                                                        • =
                                                                                                        @[reducible, inline]

                                                                                                        Task priority. Tasks with higher priority will always be scheduled before ones with lower priority.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          The default priority for spawned tasks, also the lowest priority: 0.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            The highest regular priority for spawned tasks: 8.

                                                                                                            Spawning a task with a priority higher than Task.Priority.max is not an error but will spawn a dedicated worker for the task, see Task.Priority.dedicated. Regular priority tasks are placed in a thread pool and worked on according to the priority order.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Any priority higher than Task.Priority.max will result in the task being scheduled immediately on a dedicated thread. This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more non-dedicated workers than the number of cores to reduce context switches.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[noinline, extern lean_task_spawn]
                                                                                                                def Task.spawn {α : Type u} (fn : Unitα) (prio : optParam Task.Priority Task.Priority.default) :
                                                                                                                Task α

                                                                                                                spawn fn : Task α constructs and immediately launches a new task for evaluating the function fn () : α asynchronously.

                                                                                                                prio, if provided, is the priority of the task.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[noinline, extern lean_task_map]
                                                                                                                  def Task.map {α : Type u_1} {β : Type u_2} (f : αβ) (x : Task α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                                                                                                  Task β

                                                                                                                  map f x maps function f over the task x: that is, it constructs (and immediately launches) a new task which will wait for the value of x to be available and then calls f on the result.

                                                                                                                  prio, if provided, is the priority of the task. If sync is set to true, f is executed on the current thread if x has already finished.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[noinline, extern lean_task_bind]
                                                                                                                    def Task.bind {α : Type u_1} {β : Type u_2} (x : Task α) (f : αTask β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                                                                                                    Task β

                                                                                                                    bind x f does a monad "bind" operation on the task x with function f: that is, it constructs (and immediately launches) a new task which will wait for the value of x to be available and then calls f on the result, resulting in a new task which is then run for a result.

                                                                                                                    prio, if provided, is the priority of the task. If sync is set to true, f is executed on the current thread if x has already finished.

                                                                                                                    Equations
                                                                                                                    • x.bind f prio sync = { get := (f x.get).get }
                                                                                                                    Instances For
                                                                                                                      structure NonScalar :

                                                                                                                      NonScalar is a type that is not a scalar value in our runtime. It is used as a stand-in for an arbitrary boxed value to avoid excessive monomorphization, and it is only created using unsafeCast. It is somewhat analogous to C void* in usage, but the type itself is not special.

                                                                                                                      • val : Nat

                                                                                                                        You should not use this function

                                                                                                                      Instances For
                                                                                                                        inductive PNonScalar :

                                                                                                                        PNonScalar is a type that is not a scalar value in our runtime. It is used as a stand-in for an arbitrary boxed value to avoid excessive monomorphization, and it is only created using unsafeCast. It is somewhat analogous to C void* in usage, but the type itself is not special.

                                                                                                                        This is the universe-polymorphic version of PNonScalar; it is preferred to use NonScalar instead where applicable.

                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem Nat.add_zero (n : Nat) :
                                                                                                                          n + 0 = n
                                                                                                                          theorem optParam_eq (α : Sort u) (default : α) :
                                                                                                                          optParam α default = α

                                                                                                                          Boolean operators #

                                                                                                                          @[extern lean_strict_or]
                                                                                                                          def strictOr (b₁ : Bool) (b₂ : Bool) :

                                                                                                                          strictOr is the same as or, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is true.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[extern lean_strict_and]
                                                                                                                            def strictAnd (b₁ : Bool) (b₂ : Bool) :

                                                                                                                            strictAnd is the same as and, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is false.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def bne {α : Type u} [BEq α] (a : α) (b : α) :

                                                                                                                              x != y is boolean not-equal. It is the negation of x == y which is supplied by the BEq typeclass.

                                                                                                                              Unlike x ≠ y (which is notation for Ne x y), this is Bool valued instead of Prop valued. It is mainly intended for programming applications.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                x != y is boolean not-equal. It is the negation of x == y which is supplied by the BEq typeclass.

                                                                                                                                Unlike x ≠ y (which is notation for Ne x y), this is Bool valued instead of Prop valued. It is mainly intended for programming applications.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  class LawfulBEq (α : Type u) [BEq α] :

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

                                                                                                                                  • eq_of_beq : ∀ {a b : α}, (a == b) = truea = b

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

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

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

                                                                                                                                  Instances
                                                                                                                                    theorem LawfulBEq.eq_of_beq {α : Type u} [BEq α] [self : LawfulBEq α] {a : α} {b : α} :
                                                                                                                                    (a == b) = truea = b

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

                                                                                                                                    theorem LawfulBEq.rfl {α : Type u} [BEq α] [self : LawfulBEq α] {a : α} :
                                                                                                                                    (a == a) = true

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

                                                                                                                                    instance instLawfulBEq {α : Type u_1} [DecidableEq α] :
                                                                                                                                    Equations
                                                                                                                                    • =

                                                                                                                                    Logical connectives and equality #

                                                                                                                                    theorem trivial :

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

                                                                                                                                    theorem mt {a : Prop} {b : Prop} (h₁ : ab) (h₂ : ¬b) :
                                                                                                                                    theorem not_not_intro {p : Prop} (h : p) :
                                                                                                                                    theorem proof_irrel {a : Prop} (h₁ : a) (h₂ : a) :
                                                                                                                                    h₁ = h₂
                                                                                                                                    @[macro_inline]
                                                                                                                                    def Eq.mp {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
                                                                                                                                    β

                                                                                                                                    If h : α = β is a proof of type equality, then h.mp : α → β is the induced "cast" operation, mapping elements of α to elements of β.

                                                                                                                                    You can prove theorems about the resulting element by induction on h, since rfl.mp is definitionally the identity function.

                                                                                                                                    Equations
                                                                                                                                    • h.mp a = ha
                                                                                                                                    Instances For
                                                                                                                                      @[macro_inline]
                                                                                                                                      def Eq.mpr {α : Sort u} {β : Sort u} (h : α = β) (b : β) :
                                                                                                                                      α

                                                                                                                                      If h : α = β is a proof of type equality, then h.mpr : β → α is the induced "cast" operation in the reverse direction, mapping elements of β to elements of α.

                                                                                                                                      You can prove theorems about the resulting element by induction on h, since rfl.mpr is definitionally the identity function.

                                                                                                                                      Equations
                                                                                                                                      • h.mpr b = b
                                                                                                                                      Instances For
                                                                                                                                        theorem Eq.substr {α : Sort u} {p : αProp} {a : α} {b : α} (h₁ : b = a) (h₂ : p a) :
                                                                                                                                        p b
                                                                                                                                        @[simp]
                                                                                                                                        theorem cast_eq {α : Sort u} (h : α = α) (a : α) :
                                                                                                                                        cast h a = a
                                                                                                                                        @[reducible]
                                                                                                                                        def Ne {α : Sort u} (a : α) (b : α) :

                                                                                                                                        a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            theorem Ne.intro {α : Sort u} {a : α} {b : α} (h : a = bFalse) :
                                                                                                                                            a b
                                                                                                                                            theorem Ne.elim {α : Sort u} {a : α} {b : α} (h : a b) :
                                                                                                                                            a = bFalse
                                                                                                                                            theorem Ne.irrefl {α : Sort u} {a : α} (h : a a) :
                                                                                                                                            theorem Ne.symm {α : Sort u} {a : α} {b : α} (h : a b) :
                                                                                                                                            b a
                                                                                                                                            theorem ne_comm {α : Sort u_1} {a : α} {b : α} :
                                                                                                                                            a b b a
                                                                                                                                            theorem false_of_ne {α : Sort u} {a : α} :
                                                                                                                                            a aFalse
                                                                                                                                            theorem ne_false_of_self {p : Prop} :
                                                                                                                                            pp False
                                                                                                                                            theorem ne_true_of_not {p : Prop} :
                                                                                                                                            ¬pp True
                                                                                                                                            theorem Bool.of_not_eq_true {b : Bool} :
                                                                                                                                            ¬b = trueb = false
                                                                                                                                            theorem ne_of_beq_false {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (h : (a == b) = false) :
                                                                                                                                            a b
                                                                                                                                            theorem beq_false_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (h : a b) :
                                                                                                                                            (a == b) = false
                                                                                                                                            noncomputable def HEq.ndrec {α : Sort u2} {a : α} {motive : {β : Sort u2} → βSort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) :
                                                                                                                                            motive b

                                                                                                                                            Non-dependent recursor for HEq

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              noncomputable def HEq.ndrecOn {α : Sort u2} {a : α} {motive : {β : Sort u2} → βSort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) :
                                                                                                                                              motive b

                                                                                                                                              HEq.ndrec variant

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                noncomputable def HEq.elim {α : Sort u} {a : α} {p : αSort v} {b : α} (h₁ : HEq a b) (h₂ : p a) :
                                                                                                                                                p b

                                                                                                                                                HEq.ndrec variant

                                                                                                                                                Equations
                                                                                                                                                • h₁.elim h₂ = h₂
                                                                                                                                                Instances For
                                                                                                                                                  theorem HEq.subst {α : Sort u} {β : Sort u} {a : α} {b : β} {p : (T : Sort u) → TProp} (h₁ : HEq a b) (h₂ : p α a) :
                                                                                                                                                  p β b
                                                                                                                                                  theorem HEq.symm {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
                                                                                                                                                  HEq b a
                                                                                                                                                  theorem heq_of_eq {α : Sort u} {a : α} {a' : α} (h : a = a') :
                                                                                                                                                  HEq a a'
                                                                                                                                                  theorem HEq.trans {α : Sort u} {β : Sort u} {φ : Sort u} {a : α} {b : β} {c : φ} (h₁ : HEq a b) (h₂ : HEq b c) :
                                                                                                                                                  HEq a c
                                                                                                                                                  theorem heq_of_heq_of_eq {α : Sort u} {β : Sort u} {a : α} {b : β} {b' : β} (h₁ : HEq a b) (h₂ : b = b') :
                                                                                                                                                  HEq a b'
                                                                                                                                                  theorem heq_of_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {a' : α} {b : β} (h₁ : a = a') (h₂ : HEq a' b) :
                                                                                                                                                  HEq a b
                                                                                                                                                  theorem type_eq_of_heq {α : Sort u} {β : Sort u} {a : α} {b : β} (h : HEq a b) :
                                                                                                                                                  α = β
                                                                                                                                                  theorem eqRec_heq {α : Sort u} {φ : αSort v} {a : α} {a' : α} (h : a = a') (p : φ a) :
                                                                                                                                                  HEq (Eq.recOn h p) p
                                                                                                                                                  theorem heq_of_eqRec_eq {α : Sort u} {β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : h₁a = b) :
                                                                                                                                                  HEq a b
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem cast_heq {α : Sort u} {β : Sort u} (h : α = β) (a : α) :
                                                                                                                                                  HEq (cast h a) a
                                                                                                                                                  theorem iff_iff_implies_and_implies (a : Prop) (b : Prop) :
                                                                                                                                                  (a b) (ab) (ba)
                                                                                                                                                  theorem Iff.refl (a : Prop) :
                                                                                                                                                  a a
                                                                                                                                                  theorem Iff.rfl {a : Prop} :
                                                                                                                                                  a a
                                                                                                                                                  theorem Iff.of_eq {a : Prop} {b : Prop} (h : a = b) :
                                                                                                                                                  a b
                                                                                                                                                  theorem Iff.trans {a : Prop} {b : Prop} {c : Prop} (h₁ : a b) (h₂ : b c) :
                                                                                                                                                  a c
                                                                                                                                                  Equations
                                                                                                                                                  theorem Eq.comm {α : Sort u_1} {a : α} {b : α} :
                                                                                                                                                  a = b b = a
                                                                                                                                                  theorem eq_comm {α : Sort u_1} {a : α} {b : α} :
                                                                                                                                                  a = b b = a
                                                                                                                                                  theorem Iff.symm {a : Prop} {b : Prop} (h : a b) :
                                                                                                                                                  b a
                                                                                                                                                  theorem Iff.comm {a : Prop} {b : Prop} :
                                                                                                                                                  (a b) (b a)
                                                                                                                                                  theorem iff_comm {a : Prop} {b : Prop} :
                                                                                                                                                  (a b) (b a)
                                                                                                                                                  theorem And.symm {a : Prop} {b : Prop} :
                                                                                                                                                  a bb a
                                                                                                                                                  theorem And.comm {a : Prop} {b : Prop} :
                                                                                                                                                  a b b a
                                                                                                                                                  theorem and_comm {a : Prop} {b : Prop} :
                                                                                                                                                  a b b a
                                                                                                                                                  theorem Or.symm {a : Prop} {b : Prop} :
                                                                                                                                                  a bb a
                                                                                                                                                  theorem Or.comm {a : Prop} {b : Prop} :
                                                                                                                                                  a b b a
                                                                                                                                                  theorem or_comm {a : Prop} {b : Prop} :
                                                                                                                                                  a b b a

                                                                                                                                                  Exists #

                                                                                                                                                  theorem Exists.elim {α : Sort u} {p : αProp} {b : Prop} (h₁ : ∃ (x : α), p x) (h₂ : ∀ (a : α), p ab) :
                                                                                                                                                  b

                                                                                                                                                  Decidable #

                                                                                                                                                  @[inline]
                                                                                                                                                  def toBoolUsing {p : Prop} (d : Decidable p) :

                                                                                                                                                  Similar to decide, but uses an explicit instance

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) :
                                                                                                                                                    theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) :
                                                                                                                                                    p
                                                                                                                                                    @[macro_inline]
                                                                                                                                                    def Decidable.byCases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : pq) (h2 : ¬pq) :
                                                                                                                                                    q

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

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      theorem Decidable.em (p : Prop) [Decidable p] :
                                                                                                                                                      p ¬p
                                                                                                                                                      theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬pFalse) :
                                                                                                                                                      p
                                                                                                                                                      theorem Decidable.of_not_not {p : Prop} [Decidable p] :
                                                                                                                                                      ¬¬pp
                                                                                                                                                      theorem Decidable.not_and_iff_or_not (p : Prop) (q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] :
                                                                                                                                                      ¬(p q) ¬p ¬q
                                                                                                                                                      @[inline]

                                                                                                                                                      Transfer a decidability proof across an equivalence of propositions.

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def decidable_of_decidable_of_eq {p : Prop} {q : Prop} [Decidable p] (h : p = q) :

                                                                                                                                                        Transfer a decidability proof across an equality of propositions.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[macro_inline]
                                                                                                                                                          instance instDecidableForall {p : Prop} {q : Prop} [Decidable p] [Decidable q] :
                                                                                                                                                          Decidable (pq)
                                                                                                                                                          Equations
                                                                                                                                                          instance instDecidableIff {p : Prop} {q : Prop} [Decidable p] [Decidable q] :
                                                                                                                                                          Equations

                                                                                                                                                          if-then-else expression theorems #

                                                                                                                                                          theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : α} {e : α} :
                                                                                                                                                          (if c then t else e) = t
                                                                                                                                                          theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : α} {e : α} :
                                                                                                                                                          (if c then t else e) = e
                                                                                                                                                          def iteInduction {α : Sort u_1} {c : Prop} [inst : Decidable c] {motive : αSort u_2} {t : α} {e : α} (hpos : cmotive t) (hneg : ¬cmotive e) :
                                                                                                                                                          motive (if c then t else e)

                                                                                                                                                          Split an if-then-else into cases. The split tactic is generally easier to use than this theorem.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : cα} {e : ¬cα} :
                                                                                                                                                            dite c t e = t hc
                                                                                                                                                            theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : cα} {e : ¬cα} :
                                                                                                                                                            dite c t e = e hnc
                                                                                                                                                            theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
                                                                                                                                                            (if x : c then t else e) = if c then t else e
                                                                                                                                                            instance instDecidableIte {c : Prop} {t : Prop} {e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] :
                                                                                                                                                            Decidable (if c then t else e)
                                                                                                                                                            Equations
                                                                                                                                                            • instDecidableIte = dT
                                                                                                                                                            • instDecidableIte = dE
                                                                                                                                                            instance instDecidableDite {c : Prop} {t : cProp} {e : ¬cProp} [dC : Decidable c] [dT : (h : c) → Decidable (t h)] [dE : (h : ¬c) → Decidable (e h)] :
                                                                                                                                                            Decidable (if h : c then t h else e h)
                                                                                                                                                            Equations
                                                                                                                                                            • instDecidableDite = dT h
                                                                                                                                                            • instDecidableDite = dE h
                                                                                                                                                            @[reducible, inline]
                                                                                                                                                            abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : αβ) (P : Sort w) (x : α) (y : α) :

                                                                                                                                                            Auxiliary definition for generating compact noConfusion for enumeration types

                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[reducible, inline]
                                                                                                                                                              abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : αβ) {P : Sort w} {x : α} {y : α} (h : x = y) :

                                                                                                                                                              Auxiliary definition for generating compact noConfusion for enumeration types

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Inhabited #

                                                                                                                                                                instance instInhabitedForInStep_1 :
                                                                                                                                                                {a : Type u_1} → [inst : Inhabited a] → Inhabited (ForInStep a)
                                                                                                                                                                Equations
                                                                                                                                                                Equations
                                                                                                                                                                theorem nonempty_of_exists {α : Sort u} {p : αProp} :
                                                                                                                                                                (∃ (x : α), p x)Nonempty α

                                                                                                                                                                Subsingleton #

                                                                                                                                                                class Subsingleton (α : Sort u) :

                                                                                                                                                                A "subsingleton" is a type with at most one element. In other words, it is either empty, or has a unique element. All propositions are subsingletons because of proof irrelevance, but some other types are subsingletons as well and they inherit many of the same properties as propositions. Subsingleton α is a typeclass, so it is usually used as an implicit argument and inferred by typeclass inference.

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

                                                                                                                                                                    Any two elements of a subsingleton are equal.

                                                                                                                                                                • )
                                                                                                                                                                Instances
                                                                                                                                                                  theorem Subsingleton.allEq {α : Sort u} [self : Subsingleton α] (a : α) (b : α) :
                                                                                                                                                                  a = b

                                                                                                                                                                  Any two elements of a subsingleton are equal.

                                                                                                                                                                  theorem Subsingleton.elim {α : Sort u} [h : Subsingleton α] (a : α) (b : α) :
                                                                                                                                                                  a = b
                                                                                                                                                                  theorem Subsingleton.helim {α : Sort u} {β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) :
                                                                                                                                                                  HEq a b
                                                                                                                                                                  Equations
                                                                                                                                                                  • =
                                                                                                                                                                  instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] :
                                                                                                                                                                  Equations
                                                                                                                                                                  • =
                                                                                                                                                                  Equations
                                                                                                                                                                  • =
                                                                                                                                                                  theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : pSort u} {h₂ : ¬pSort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :
                                                                                                                                                                  structure Equivalence {α : Sort u} (r : ααProp) :

                                                                                                                                                                  An equivalence relation ~ : α → α → Prop is a relation that is:

                                                                                                                                                                  • reflexive: x ~ x
                                                                                                                                                                  • symmetric: x ~ y implies y ~ x
                                                                                                                                                                  • transitive: x ~ y and y ~ z implies x ~ z

                                                                                                                                                                  Equality is an equivalence relation, and equivalence relations share many of the properties of equality. In particular, Quot α r is most well behaved when r is an equivalence relation, and in this case we use Quotient instead.

                                                                                                                                                                  • refl : ∀ (x : α), r x x

                                                                                                                                                                    An equivalence relation is reflexive: x ~ x

                                                                                                                                                                  • symm : ∀ {x y : α}, r x yr y x

                                                                                                                                                                    An equivalence relation is symmetric: x ~ y implies y ~ x

                                                                                                                                                                  • trans : ∀ {x y z : α}, r x yr y zr x z

                                                                                                                                                                    An equivalence relation is transitive: x ~ y and y ~ z implies x ~ z

                                                                                                                                                                  Instances For
                                                                                                                                                                    theorem Equivalence.refl {α : Sort u} {r : ααProp} (self : Equivalence r) (x : α) :
                                                                                                                                                                    r x x

                                                                                                                                                                    An equivalence relation is reflexive: x ~ x

                                                                                                                                                                    theorem Equivalence.symm {α : Sort u} {r : ααProp} (self : Equivalence r) {x : α} {y : α} :
                                                                                                                                                                    r x yr y x

                                                                                                                                                                    An equivalence relation is symmetric: x ~ y implies y ~ x

                                                                                                                                                                    theorem Equivalence.trans {α : Sort u} {r : ααProp} (self : Equivalence r) {x : α} {y : α} {z : α} :
                                                                                                                                                                    r x yr y zr x z

                                                                                                                                                                    An equivalence relation is transitive: x ~ y and y ~ z implies x ~ z

                                                                                                                                                                    def emptyRelation {α : Sort u} :
                                                                                                                                                                    ααProp

                                                                                                                                                                    The empty relation is the relation on α which is always False.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      def Subrelation {α : Sort u} (q : ααProp) (r : ααProp) :

                                                                                                                                                                      Subrelation q r means that q ⊆ r or ∀ x y, q x y → r x y. It is the analogue of the subset relation on relations.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        def InvImage {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) :
                                                                                                                                                                        ααProp

                                                                                                                                                                        The inverse image of r : β → β → Prop by a function α → β is the relation s : α → α → Prop defined by s a b = r (f a) (f b).

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          inductive Relation.TransGen {α : Sort u} (r : ααProp) :
                                                                                                                                                                          ααProp

                                                                                                                                                                          The transitive closure TransGen r of a relation r is the smallest relation which is transitive and contains r. TransGen r a z if and only if there exists a sequence a r b r ... r z of length at least 1 connecting a to z.

                                                                                                                                                                          Instances For
                                                                                                                                                                            @[reducible, inline, deprecated Relation.TransGen]
                                                                                                                                                                            abbrev TC {α : Sort u_1} (r : ααProp) :
                                                                                                                                                                            ααProp

                                                                                                                                                                            Deprecated synonym for Relation.TransGen.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              theorem Relation.TransGen.trans {α : Sort u} {r : ααProp} {a : α} {b : α} {c : α} :

                                                                                                                                                                              Subtype #

                                                                                                                                                                              theorem Subtype.existsOfSubtype {α : Type u} {p : αProp} :
                                                                                                                                                                              { x : α // p x }∃ (x : α), p x
                                                                                                                                                                              theorem Subtype.eq {α : Type u} {p : αProp} {a1 : { x : α // p x }} {a2 : { x : α // p x }} :
                                                                                                                                                                              a1.val = a2.vala1 = a2
                                                                                                                                                                              theorem Subtype.eta {α : Type u} {p : αProp} (a : { x : α // p x }) (h : p a.val) :
                                                                                                                                                                              a.val, h = a
                                                                                                                                                                              instance Subtype.instDecidableEq {α : Type u} {p : αProp} [DecidableEq α] :
                                                                                                                                                                              DecidableEq { x : α // p x }
                                                                                                                                                                              Equations
                                                                                                                                                                              • b, h₂.instDecidableEq b_1, h₂_1 = if h : b = b_1 then isTrue else isFalse

                                                                                                                                                                              Sum #

                                                                                                                                                                              instance Sum.inhabitedLeft {α : Type u} {β : Type v} [Inhabited α] :
                                                                                                                                                                              Inhabited (α β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • Sum.inhabitedLeft = { default := Sum.inl default }
                                                                                                                                                                              instance Sum.inhabitedRight {α : Type u} {β : Type v} [Inhabited β] :
                                                                                                                                                                              Inhabited (α β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • Sum.inhabitedRight = { default := Sum.inr default }
                                                                                                                                                                              instance instDecidableEqSum {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] :
                                                                                                                                                                              Equations

                                                                                                                                                                              Product #

                                                                                                                                                                              instance instInhabitedProd {α : Type u_1} {β : Type u_2} [Inhabited α] [Inhabited β] :
                                                                                                                                                                              Inhabited (α × β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • instInhabitedProd = { default := (default, default) }
                                                                                                                                                                              instance instInhabitedMProd {α : Type u_1} {β : Type u_1} [Inhabited α] [Inhabited β] :
                                                                                                                                                                              Equations
                                                                                                                                                                              • instInhabitedMProd = { default := default, default }
                                                                                                                                                                              instance instInhabitedPProd {α : Sort u_1} {β : Sort u_2} [Inhabited α] [Inhabited β] :
                                                                                                                                                                              Inhabited (α ×' β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • instInhabitedPProd = { default := default, default }
                                                                                                                                                                              instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] :
                                                                                                                                                                              DecidableEq (α × β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              instance instBEqProd {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :
                                                                                                                                                                              BEq (α × β)
                                                                                                                                                                              Equations
                                                                                                                                                                              • instBEqProd = { beq := fun (x x_1 : α × β) => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => a₁ == a₂ && b₁ == b₂ }
                                                                                                                                                                              def Prod.lexLt {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : α × β) (t : α × β) :

                                                                                                                                                                              Lexicographical order for products

                                                                                                                                                                              Equations
                                                                                                                                                                              • s.lexLt t = (s.fst < t.fst s.fst = t.fst s.snd < t.snd)
                                                                                                                                                                              Instances For
                                                                                                                                                                                instance Prod.lexLtDec {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DecidableEq α] [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)] (s : α × β) (t : α × β) :
                                                                                                                                                                                Decidable (s.lexLt t)
                                                                                                                                                                                Equations
                                                                                                                                                                                theorem Prod.lexLt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s : α × β) (t : α × β) :
                                                                                                                                                                                s.lexLt t = (s.fst < t.fst s.fst = t.fst s.snd < t.snd)
                                                                                                                                                                                theorem Prod.eta {α : Type u_1} {β : Type u_2} (p : α × β) :
                                                                                                                                                                                (p.fst, p.snd) = p
                                                                                                                                                                                def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁α₂) (g : β₁β₂) :
                                                                                                                                                                                α₁ × β₁α₂ × β₂

                                                                                                                                                                                Prod.map f g : α₁ × β₁ → α₂ × β₂ maps across a pair by applying f to the first component and g to the second.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Prod.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α) (y : γ) :
                                                                                                                                                                                  Prod.map f g (x, y) = (f x, g y)
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Prod.map_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α × γ) :
                                                                                                                                                                                  (Prod.map f g x).fst = f x.fst
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Prod.map_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α × γ) :
                                                                                                                                                                                  (Prod.map f g x).snd = g x.snd

                                                                                                                                                                                  Dependent products #

                                                                                                                                                                                  theorem Exists.of_psigma_prop {α : Sort u} {p : αProp} :
                                                                                                                                                                                  (x : α) ×' p x∃ (x : α), p x
                                                                                                                                                                                  @[deprecated Exists.of_psigma_prop]
                                                                                                                                                                                  theorem ex_of_PSigma {α : Type u} {p : αProp} :
                                                                                                                                                                                  (x : α) ×' p x∃ (x : α), p x
                                                                                                                                                                                  theorem PSigma.eta {α : Sort u} {β : αSort v} {a₁ : α} {a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂) (h₂ : h₁b₁ = b₂) :
                                                                                                                                                                                  a₁, b₁ = a₂, b₂

                                                                                                                                                                                  Universe polymorphic unit #

                                                                                                                                                                                  theorem PUnit.subsingleton (a : PUnit) (b : PUnit) :
                                                                                                                                                                                  a = b

                                                                                                                                                                                  Setoid #

                                                                                                                                                                                  class Setoid (α : Sort u) :
                                                                                                                                                                                  Sort (max 1 u)

                                                                                                                                                                                  A setoid is a type with a distinguished equivalence relation, denoted . This is mainly used as input to the Quotient type constructor.

                                                                                                                                                                                  • r : ααProp

                                                                                                                                                                                    x ≈ y is the distinguished equivalence relation of a setoid.

                                                                                                                                                                                  • iseqv : Equivalence Setoid.r

                                                                                                                                                                                    The relation x ≈ y is an equivalence relation.

                                                                                                                                                                                  Instances
                                                                                                                                                                                    theorem Setoid.iseqv {α : Sort u} [self : Setoid α] :
                                                                                                                                                                                    Equivalence Setoid.r

                                                                                                                                                                                    The relation x ≈ y is an equivalence relation.

                                                                                                                                                                                    instance instHasEquivOfSetoid {α : Sort u} [Setoid α] :
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • instHasEquivOfSetoid = { Equiv := Setoid.r }
                                                                                                                                                                                    theorem Setoid.refl {α : Sort u} [Setoid α] (a : α) :
                                                                                                                                                                                    a a
                                                                                                                                                                                    theorem Setoid.symm {α : Sort u} [Setoid α] {a : α} {b : α} (hab : a b) :
                                                                                                                                                                                    b a
                                                                                                                                                                                    theorem Setoid.trans {α : Sort u} [Setoid α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
                                                                                                                                                                                    a c

                                                                                                                                                                                    Propositional extensionality #

                                                                                                                                                                                    axiom propext {a : Prop} {b : Prop} :
                                                                                                                                                                                    (a b)a = b

                                                                                                                                                                                    The axiom of propositional extensionality. It asserts that if propositions a and b are logically equivalent (i.e. we can prove a from b and vice versa), then a and b are equal, meaning that we can replace a with b in all contexts.

                                                                                                                                                                                    For simple expressions like a ∧ c ∨ d → e we can prove that because all the logical connectives respect logical equivalence, we can replace a with b in this expression without using propext. However, for higher order expressions like P a where P : Prop → Prop is unknown, or indeed for a = b itself, we cannot replace a with b without an axiom which says exactly this.

                                                                                                                                                                                    This is a relatively uncontroversial axiom, which is intuitionistically valid. It does however block computation when using #reduce to reduce proofs directly (which is not recommended), meaning that canonicity, the property that all closed terms of type Nat normalize to numerals, fails to hold when this (or any) axiom is used:

                                                                                                                                                                                    set_option pp.proofs true
                                                                                                                                                                                    
                                                                                                                                                                                    def foo : Nat := by
                                                                                                                                                                                      have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
                                                                                                                                                                                      have := propext this ▸ (2 : Nat)
                                                                                                                                                                                      exact this
                                                                                                                                                                                    
                                                                                                                                                                                    #reduce foo
                                                                                                                                                                                    -- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
                                                                                                                                                                                    
                                                                                                                                                                                    #eval foo -- 2
                                                                                                                                                                                    

                                                                                                                                                                                    #eval can evaluate it to a numeral because the compiler erases casts and does not evaluate proofs, so propext, whose return type is a proposition, can never block it.

                                                                                                                                                                                    theorem Eq.propIntro {a : Prop} {b : Prop} (h₁ : ab) (h₂ : ba) :
                                                                                                                                                                                    a = b
                                                                                                                                                                                    instance instDecidableEqOfIff {p : Prop} {q : Prop} [d : Decidable (p q)] :
                                                                                                                                                                                    Decidable (p = q)
                                                                                                                                                                                    Equations
                                                                                                                                                                                    theorem Nat.succ.inj {m : Nat} {n : Nat} :
                                                                                                                                                                                    m.succ = n.succm = n
                                                                                                                                                                                    theorem Nat.succ.injEq (u : Nat) (v : Nat) :
                                                                                                                                                                                    (u.succ = v.succ) = (u = v)
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem beq_iff_eq {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) :
                                                                                                                                                                                    (a == b) = true a = b

                                                                                                                                                                                    Prop lemmas #

                                                                                                                                                                                    def Not.elim {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) :
                                                                                                                                                                                    α

                                                                                                                                                                                    Ex falso for negation: from ¬a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the Not namespace so that projection notation can be used.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                      abbrev And.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : abα) (h : a b) :
                                                                                                                                                                                      α

                                                                                                                                                                                      Non-dependent eliminator for And.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def Iff.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : (ab)(ba)α) (h : a b) :
                                                                                                                                                                                        α

                                                                                                                                                                                        Non-dependent eliminator for Iff.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          theorem Iff.subst {a : Prop} {b : Prop} {p : PropProp} (h₁ : a b) (h₂ : p a) :
                                                                                                                                                                                          p b

                                                                                                                                                                                          Iff can now be used to do substitutions in a calculation

                                                                                                                                                                                          theorem Not.intro {a : Prop} (h : aFalse) :
                                                                                                                                                                                          theorem Not.imp {a : Prop} {b : Prop} (H2 : ¬b) (H1 : ab) :
                                                                                                                                                                                          theorem not_congr {a : Prop} {b : Prop} (h : a b) :
                                                                                                                                                                                          theorem iff_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :
                                                                                                                                                                                          a b
                                                                                                                                                                                          theorem iff_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
                                                                                                                                                                                          a b
                                                                                                                                                                                          theorem iff_true_left {a : Prop} {b : Prop} (ha : a) :
                                                                                                                                                                                          (a b) b
                                                                                                                                                                                          theorem iff_true_right {a : Prop} {b : Prop} (ha : a) :
                                                                                                                                                                                          (b a) b
                                                                                                                                                                                          theorem iff_false_left {a : Prop} {b : Prop} (ha : ¬a) :
                                                                                                                                                                                          (a b) ¬b
                                                                                                                                                                                          theorem iff_false_right {a : Prop} {b : Prop} (ha : ¬a) :
                                                                                                                                                                                          (b a) ¬b
                                                                                                                                                                                          theorem of_iff_true {a : Prop} (h : a True) :
                                                                                                                                                                                          a
                                                                                                                                                                                          theorem iff_true_intro {a : Prop} (h : a) :
                                                                                                                                                                                          theorem eq_iff_true_of_subsingleton {α : Sort u_1} [Subsingleton α] (x : α) (y : α) :
                                                                                                                                                                                          x = y True
                                                                                                                                                                                          theorem not_of_iff_false {p : Prop} :
                                                                                                                                                                                          (p False)¬p
                                                                                                                                                                                          theorem iff_false_intro {a : Prop} (h : ¬a) :
                                                                                                                                                                                          theorem not_iff_false_intro {a : Prop} (h : a) :
                                                                                                                                                                                          theorem Eq.to_iff {a : Prop} {b : Prop} :
                                                                                                                                                                                          a = b(a b)
                                                                                                                                                                                          theorem iff_of_eq {a : Prop} {b : Prop} :
                                                                                                                                                                                          a = b(a b)
                                                                                                                                                                                          theorem neq_of_not_iff {a : Prop} {b : Prop} :
                                                                                                                                                                                          ¬(a b)a b
                                                                                                                                                                                          theorem iff_iff_eq {a : Prop} {b : Prop} :
                                                                                                                                                                                          (a b) a = b
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem eq_iff_iff {a : Prop} {b : Prop} :
                                                                                                                                                                                          a = b (a b)
                                                                                                                                                                                          theorem eq_self_iff_true {α : Sort u_1} (a : α) :
                                                                                                                                                                                          a = a True
                                                                                                                                                                                          theorem ne_self_iff_false {α : Sort u_1} (a : α) :
                                                                                                                                                                                          theorem iff_def {a : Prop} {b : Prop} :
                                                                                                                                                                                          (a b) (ab) (ba)
                                                                                                                                                                                          theorem iff_def' {a : Prop} {b : Prop} :
                                                                                                                                                                                          (a b) (ba) (ab)
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem iff_not_self {a : Prop} :
                                                                                                                                                                                          ¬(a ¬a)
                                                                                                                                                                                          theorem heq_self_iff_true {α : Sort u_1} (a : α) :

                                                                                                                                                                                          implies #

                                                                                                                                                                                          theorem not_not_of_not_imp {a : Prop} {b : Prop} :
                                                                                                                                                                                          ¬(ab)¬¬a
                                                                                                                                                                                          theorem not_of_not_imp {b : Prop} {a : Prop} :
                                                                                                                                                                                          ¬(ab)¬b
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem imp_not_self {a : Prop} :
                                                                                                                                                                                          a¬a ¬a
                                                                                                                                                                                          theorem imp_intro {α : Prop} {β : Prop} (h : α) :
                                                                                                                                                                                          βα
                                                                                                                                                                                          theorem imp_imp_imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₀ : ca) (h₁ : bd) :
                                                                                                                                                                                          (ab)cd
                                                                                                                                                                                          theorem imp_iff_right {b : Prop} {a : Prop} (ha : a) :
                                                                                                                                                                                          ab b
                                                                                                                                                                                          theorem imp_true_iff (α : Sort u) :
                                                                                                                                                                                          αTrue True
                                                                                                                                                                                          theorem false_imp_iff (a : Prop) :
                                                                                                                                                                                          Falsea True
                                                                                                                                                                                          theorem true_imp_iff (α : Prop) :
                                                                                                                                                                                          Trueα α
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem imp_self {a : Prop} :
                                                                                                                                                                                          aa True
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem imp_false {a : Prop} :
                                                                                                                                                                                          aFalse ¬a
                                                                                                                                                                                          theorem imp.swap {a : Prop} {b : Prop} {c : Prop} :
                                                                                                                                                                                          abc bac
                                                                                                                                                                                          theorem imp_not_comm {a : Prop} {b : Prop} :
                                                                                                                                                                                          a¬b b¬a
                                                                                                                                                                                          theorem imp_congr_left {a : Prop} {b : Prop} {c : Prop} (h : a b) :
                                                                                                                                                                                          ac bc
                                                                                                                                                                                          theorem imp_congr_right {a : Prop} {b : Prop} {c : Prop} (h : a(b c)) :
                                                                                                                                                                                          ab ac
                                                                                                                                                                                          theorem imp_congr_ctx {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a c) (h₂ : c(b d)) :
                                                                                                                                                                                          ab cd
                                                                                                                                                                                          theorem imp_congr {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
                                                                                                                                                                                          ab cd
                                                                                                                                                                                          theorem imp_iff_not {a : Prop} {b : Prop} (hb : ¬b) :
                                                                                                                                                                                          ab ¬a

                                                                                                                                                                                          Quotients #

                                                                                                                                                                                          axiom Quot.sound {α : Sort u} {r : ααProp} {a : α} {b : α} :
                                                                                                                                                                                          r a bQuot.mk r a = Quot.mk r b

                                                                                                                                                                                          The quotient axiom, or at least the nontrivial part of the quotient axiomatization. Quotient types are introduced by the init_quot command in Init.Prelude which introduces the axioms:

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

                                                                                                                                                                                          All of these axioms are true if we assume Quot α r = α and Quot.mk and Quot.lift are identity functions, so they do not add much. However this axiom cannot be explained in that way (it is false for that interpretation), so the real power of quotient types come from this axiom.

                                                                                                                                                                                          It says that the quotient by r maps elements which are related by r to equal values in the quotient. Together with Quot.lift which says that functions which respect r can be lifted to functions on the quotient, we can deduce that Quot α r exactly consists of the equivalence classes with respect to r.

                                                                                                                                                                                          It is important to note that r need not be an equivalence relation in this axiom. When r is not an equivalence relation, we are actually taking a quotient with respect to the equivalence relation generated by r.

                                                                                                                                                                                          theorem Quot.liftBeta {α : Sort u} {r : ααProp} {β : Sort v} (f : αβ) (c : ∀ (a b : α), r a bf a = f b) (a : α) :
                                                                                                                                                                                          Quot.lift f c (Quot.mk r a) = f a
                                                                                                                                                                                          theorem Quot.indBeta {α : Sort u} {r : ααProp} {motive : Quot rProp} (p : ∀ (a : α), motive (Quot.mk r a)) (a : α) :
                                                                                                                                                                                          =
                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                          abbrev Quot.liftOn {α : Sort u} {β : Sort v} {r : ααProp} (q : Quot r) (f : αβ) (c : ∀ (a b : α), r a bf a = f b) :
                                                                                                                                                                                          β

                                                                                                                                                                                          Quot.liftOn q f h is the same as Quot.lift f h q. It just reorders the argument q : Quot r to be first.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            theorem Quot.inductionOn {α : Sort u} {r : ααProp} {motive : Quot rProp} (q : Quot r) (h : ∀ (a : α), motive (Quot.mk r a)) :
                                                                                                                                                                                            motive q
                                                                                                                                                                                            theorem Quot.exists_rep {α : Sort u} {r : ααProp} (q : Quot r) :
                                                                                                                                                                                            ∃ (a : α), Quot.mk r a = q
                                                                                                                                                                                            @[reducible, macro_inline]
                                                                                                                                                                                            def Quot.indep {α : Sort u} {r : ααProp} {motive : Quot rSort v} (f : (a : α) → motive (Quot.mk r a)) (a : α) :
                                                                                                                                                                                            PSigma motive

                                                                                                                                                                                            Auxiliary definition for Quot.rec.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              theorem Quot.indepCoherent {α : Sort u} {r : ααProp} {motive : Quot rSort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) (a : α) (b : α) :
                                                                                                                                                                                              r a bQuot.indep f a = Quot.indep f b
                                                                                                                                                                                              theorem Quot.liftIndepPr1 {α : Sort u} {r : ααProp} {motive : Quot rSort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) (q : Quot r) :
                                                                                                                                                                                              (Quot.lift (Quot.indep f) q).fst = q
                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                              abbrev Quot.rec {α : Sort u} {r : ααProp} {motive : Quot rSort v} (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) (q : Quot r) :
                                                                                                                                                                                              motive q

                                                                                                                                                                                              Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                abbrev Quot.recOn {α : Sort u} {r : ααProp} {motive : Quot rSort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) :
                                                                                                                                                                                                motive q

                                                                                                                                                                                                Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                  abbrev Quot.recOnSubsingleton {α : Sort u} {r : ααProp} {motive : Quot rSort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :
                                                                                                                                                                                                  motive q

                                                                                                                                                                                                  Dependent induction principle for a quotient, when the target type is a Subsingleton. In this case the quotient's side condition is trivial so any function can be lifted.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                                                    abbrev Quot.hrecOn {α : Sort u} {r : ααProp} {motive : Quot rSort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (c : ∀ (a b : α), r a bHEq (f a) (f b)) :
                                                                                                                                                                                                    motive q

                                                                                                                                                                                                    Heterogeneous dependent recursion principle for a quotient. This may be easier to work with since it uses HEq instead of an Eq.ndrec in the hypothesis.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def Quotient {α : Sort u} (s : Setoid α) :

                                                                                                                                                                                                      Quotient α s is the same as Quot α r, but it is specialized to a setoid s (that is, an equivalence relation) instead of an arbitrary relation. Prefer Quotient over Quot if your relation is actually an equivalence relation.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        def Quotient.mk {α : Sort u} (s : Setoid α) (a : α) :

                                                                                                                                                                                                        The canonical quotient map into a Quotient.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          def Quotient.mk' {α : Sort u} [s : Setoid α] (a : α) :

                                                                                                                                                                                                          The canonical quotient map into a Quotient. (This synthesizes the setoid by typeclass inference.)

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            theorem Quotient.sound {α : Sort u} {s : Setoid α} {a : α} {b : α} :
                                                                                                                                                                                                            a bQuotient.mk s a = Quotient.mk s b

                                                                                                                                                                                                            The analogue of Quot.sound: If a and b are related by the equivalence relation, then they have equal equivalence classes.

                                                                                                                                                                                                            @[reducible, inline]
                                                                                                                                                                                                            abbrev Quotient.lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : αβ) :
                                                                                                                                                                                                            (∀ (a b : α), a bf a = f b)Quotient sβ

                                                                                                                                                                                                            The analogue of Quot.lift: if f : α → β respects the equivalence relation , then it lifts to a function on Quotient s such that lift f h (mk a) = f a.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              theorem Quotient.ind {α : Sort u} {s : Setoid α} {motive : Quotient sProp} :
                                                                                                                                                                                                              (∀ (a : α), motive (Quotient.mk s a))∀ (q : Quotient s), motive q

                                                                                                                                                                                                              The analogue of Quot.ind: every element of Quotient s is of the form Quotient.mk s a.

                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                              abbrev Quotient.liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : αβ) (c : ∀ (a b : α), a bf a = f b) :
                                                                                                                                                                                                              β

                                                                                                                                                                                                              The analogue of Quot.liftOn: if f : α → β respects the equivalence relation , then it lifts to a function on Quotient s such that liftOn (mk a) f h = f a.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                theorem Quotient.inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient sProp} (q : Quotient s) (h : ∀ (a : α), motive (Quotient.mk s a)) :
                                                                                                                                                                                                                motive q

                                                                                                                                                                                                                The analogue of Quot.inductionOn: every element of Quotient s is of the form Quotient.mk s a.

                                                                                                                                                                                                                theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) :
                                                                                                                                                                                                                ∃ (a : α), Quotient.mk s a = q
                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                def Quotient.rec {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α) (p : a b), f a = f b) (q : Quotient s) :
                                                                                                                                                                                                                motive q

                                                                                                                                                                                                                The analogue of Quot.rec for Quotient. See Quot.rec.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                  abbrev Quotient.recOn {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α) (p : a b), f a = f b) :
                                                                                                                                                                                                                  motive q

                                                                                                                                                                                                                  The analogue of Quot.recOn for Quotient. See Quot.recOn.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                                                                    abbrev Quotient.recOnSubsingleton {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))] (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) :
                                                                                                                                                                                                                    motive q

                                                                                                                                                                                                                    The analogue of Quot.recOnSubsingleton for Quotient. See Quot.recOnSubsingleton.

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                      abbrev Quotient.hrecOn {α : Sort u} {s : Setoid α} {motive : Quotient sSort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (c : ∀ (a b : α), a bHEq (f a) (f b)) :
                                                                                                                                                                                                                      motive q

                                                                                                                                                                                                                      The analogue of Quot.hrecOn for Quotient. See Quot.hrecOn.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                                                                        abbrev Quotient.lift₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (f : αβφ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
                                                                                                                                                                                                                        φ

                                                                                                                                                                                                                        Lift a binary function to a quotient on both arguments.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                          abbrev Quotient.liftOn₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : αβφ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) :
                                                                                                                                                                                                                          φ

                                                                                                                                                                                                                          Lift a binary function to a quotient on both arguments.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            theorem Quotient.ind₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁Quotient s₂Prop} (h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
                                                                                                                                                                                                                            motive q₁ q₂
                                                                                                                                                                                                                            theorem Quotient.inductionOn₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
                                                                                                                                                                                                                            motive q₁ q₂
                                                                                                                                                                                                                            theorem Quotient.inductionOn₃ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ} {motive : Quotient s₁Quotient s₂Quotient s₃Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)) :
                                                                                                                                                                                                                            motive q₁ q₂ q₃
                                                                                                                                                                                                                            theorem Quotient.exact {α : Sort u} {s : Setoid α} {a : α} {b : α} :
                                                                                                                                                                                                                            Quotient.mk s a = Quotient.mk s ba b
                                                                                                                                                                                                                            @[reducible, inline]
                                                                                                                                                                                                                            abbrev Quotient.recOnSubsingleton₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁Quotient s₂Sort uC} [s : ∀ (a : α) (b : β), Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (g : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
                                                                                                                                                                                                                            motive q₁ q₂

                                                                                                                                                                                                                            Lift a binary function to a quotient on both arguments.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              instance instDecidableEqQuotientOfDecidableEquiv {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a b)] :
                                                                                                                                                                                                                              Equations

                                                                                                                                                                                                                              Function extensionality #

                                                                                                                                                                                                                              theorem funext {α : Sort u} {β : αSort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : ∀ (x : α), f x = g x) :
                                                                                                                                                                                                                              f = g

                                                                                                                                                                                                                              Function extensionality is the statement that if two functions take equal values every point, then the functions themselves are equal: (∀ x, f x = g x) → f = g. It is called "extensionality" because it talks about how to prove two objects are equal based on the properties of the object (compare with set extensionality, which is (∀ x, x ∈ s ↔ x ∈ t) → s = t).

                                                                                                                                                                                                                              This is often an axiom in dependent type theory systems, because it cannot be proved from the core logic alone. However in lean's type theory this follows from the existence of quotient types (note the Quot.sound in the proof, as well as the show line which makes use of the definitional equality Quot.lift f h (Quot.mk x) = f x).

                                                                                                                                                                                                                              instance instSubsingletonForall {α : Sort u} {β : αSort v} [∀ (a : α), Subsingleton (β a)] :
                                                                                                                                                                                                                              Subsingleton ((a : α) → β a)
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • =

                                                                                                                                                                                                                              Squash #

                                                                                                                                                                                                                              def Squash (α : Type u) :

                                                                                                                                                                                                                              Squash α is the quotient of α by the always true relation. It is empty if α is empty, otherwise it is a singleton. (Thus it is unconditionally a Subsingleton.) It is the "universal Subsingleton" mapped from α.

                                                                                                                                                                                                                              It is similar to Nonempty α, which has the same properties, but unlike Nonempty this is a Type u, that is, it is "data", and the compiler represents an element of Squash α the same as α itself (as compared to Nonempty α, whose elements are represented by a dummy value).

                                                                                                                                                                                                                              Squash.lift will extract a value in any subsingleton β from a function on α, while Nonempty.rec can only do the same when β is a proposition.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                def Squash.mk {α : Type u} (x : α) :

                                                                                                                                                                                                                                The canonical quotient map into Squash α.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  theorem Squash.ind {α : Type u} {motive : Squash αProp} (h : ∀ (a : α), motive (Squash.mk a)) (q : Squash α) :
                                                                                                                                                                                                                                  motive q
                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                  def Squash.lift {α : Type u_1} {β : Sort u_2} [Subsingleton β] (s : Squash α) (f : αβ) :
                                                                                                                                                                                                                                  β

                                                                                                                                                                                                                                  If β is a subsingleton, then a function α → β lifts to Squash α → β.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    • =

                                                                                                                                                                                                                                    Relations #

                                                                                                                                                                                                                                    class Antisymm {α : Sort u} (r : ααProp) :

                                                                                                                                                                                                                                    Antisymm (·≤·) says that (·≤·) is antisymmetric, that is, a ≤ b → b ≤ a → a = b.

                                                                                                                                                                                                                                    • antisymm : ∀ {a b : α}, r a br b aa = b

                                                                                                                                                                                                                                      An antisymmetric relation (·≤·) satisfies a ≤ b → b ≤ a → a = b.

                                                                                                                                                                                                                                    Instances
                                                                                                                                                                                                                                      theorem Antisymm.antisymm {α : Sort u} {r : ααProp} [self : Antisymm r] {a : α} {b : α} :
                                                                                                                                                                                                                                      r a br b aa = b

                                                                                                                                                                                                                                      An antisymmetric relation (·≤·) satisfies a ≤ b → b ≤ a → a = b.

                                                                                                                                                                                                                                      Kernel reduction hints #

                                                                                                                                                                                                                                      Depends on the correctness of the Lean compiler, interpreter, and all [implemented_by ...] and [extern ...] annotations.

                                                                                                                                                                                                                                      opaque Lean.reduceBool (b : Bool) :

                                                                                                                                                                                                                                      When the kernel tries to reduce a term Lean.reduceBool c, it will invoke the Lean interpreter to evaluate c. The kernel will not use the interpreter if c is not a constant. This feature is useful for performing proofs by reflection.

                                                                                                                                                                                                                                      Remark: the Lean frontend allows terms of the from Lean.reduceBool t where t is a term not containing free variables. The frontend automatically declares a fresh auxiliary constant c and replaces the term with Lean.reduceBool c. The main motivation is that the code for t will be pre-compiled.

                                                                                                                                                                                                                                      Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

                                                                                                                                                                                                                                      Recall that the compiler trusts the correctness of all [implemented_by ...] and [extern ...] annotations. If an extern function is executed, then the trusted code base will also include the implementation of the associated foreign function.

                                                                                                                                                                                                                                      opaque Lean.reduceNat (n : Nat) :

                                                                                                                                                                                                                                      Similar to Lean.reduceBool for closed Nat terms.

                                                                                                                                                                                                                                      Remark: we do not have plans for supporting a generic reduceValue {α} (a : α) : α := a. The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression. We believe Lean.reduceBool enables most interesting applications (e.g., proof by reflection).

                                                                                                                                                                                                                                      axiom Lean.ofReduceBool (a : Bool) (b : Bool) (h : Lean.reduceBool a = b) :
                                                                                                                                                                                                                                      a = b

                                                                                                                                                                                                                                      The axiom ofReduceBool is used to perform proofs by reflection. See reduceBool.

                                                                                                                                                                                                                                      This axiom is usually not used directly, because it has some syntactic restrictions. Instead, the native_decide tactic can be used to prove any proposition whose decidability instance can be evaluated to true using the lean compiler / interpreter.

                                                                                                                                                                                                                                      Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

                                                                                                                                                                                                                                      axiom Lean.ofReduceNat (a : Nat) (b : Nat) (h : Lean.reduceNat a = b) :
                                                                                                                                                                                                                                      a = b

                                                                                                                                                                                                                                      The axiom ofReduceNat is used to perform proofs by reflection. See reduceBool.

                                                                                                                                                                                                                                      Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

                                                                                                                                                                                                                                      @[simp]
                                                                                                                                                                                                                                      theorem ge_iff_le {α : Type u} [LE α] {x : α} {y : α} :
                                                                                                                                                                                                                                      x y y x
                                                                                                                                                                                                                                      @[simp]
                                                                                                                                                                                                                                      theorem gt_iff_lt {α : Type u} [LT α] {x : α} {y : α} :
                                                                                                                                                                                                                                      x > y y < x
                                                                                                                                                                                                                                      theorem le_of_eq_of_le {α : Type u} {a : α} {b : α} {c : α} [LE α] (h₁ : a = b) (h₂ : b c) :
                                                                                                                                                                                                                                      a c
                                                                                                                                                                                                                                      theorem le_of_le_of_eq {α : Type u} {a : α} {b : α} {c : α} [LE α] (h₁ : a b) (h₂ : b = c) :
                                                                                                                                                                                                                                      a c
                                                                                                                                                                                                                                      theorem lt_of_eq_of_lt {α : Type u} {a : α} {b : α} {c : α} [LT α] (h₁ : a = b) (h₂ : b < c) :
                                                                                                                                                                                                                                      a < c
                                                                                                                                                                                                                                      theorem lt_of_lt_of_eq {α : Type u} {a : α} {b : α} {c : α} [LT α] (h₁ : a < b) (h₂ : b = c) :
                                                                                                                                                                                                                                      a < c
                                                                                                                                                                                                                                      class Std.Associative {α : Sort u} (op : ααα) :

                                                                                                                                                                                                                                      Associative op indicates op is an associative operation, i.e. (a ∘ b) ∘ c = a ∘ (b ∘ c).

                                                                                                                                                                                                                                      • assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

                                                                                                                                                                                                                                        An associative operation satisfies (a ∘ b) ∘ c = a ∘ (b ∘ c).

                                                                                                                                                                                                                                      Instances
                                                                                                                                                                                                                                        theorem Std.Associative.assoc {α : Sort u} {op : ααα} [self : Std.Associative op] (a : α) (b : α) (c : α) :
                                                                                                                                                                                                                                        op (op a b) c = op a (op b c)

                                                                                                                                                                                                                                        An associative operation satisfies (a ∘ b) ∘ c = a ∘ (b ∘ c).

                                                                                                                                                                                                                                        class Std.Commutative {α : Sort u} (op : ααα) :

                                                                                                                                                                                                                                        Commutative op says that op is a commutative operation, i.e. a ∘ b = b ∘ a.

                                                                                                                                                                                                                                        • comm : ∀ (a b : α), op a b = op b a

                                                                                                                                                                                                                                          A commutative operation satisfies a ∘ b = b ∘ a.

                                                                                                                                                                                                                                        Instances
                                                                                                                                                                                                                                          theorem Std.Commutative.comm {α : Sort u} {op : ααα} [self : Std.Commutative op] (a : α) (b : α) :
                                                                                                                                                                                                                                          op a b = op b a

                                                                                                                                                                                                                                          A commutative operation satisfies a ∘ b = b ∘ a.

                                                                                                                                                                                                                                          class Std.IdempotentOp {α : Sort u} (op : ααα) :

                                                                                                                                                                                                                                          IdempotentOp op indicates op is an idempotent binary operation. i.e. a ∘ a = a.

                                                                                                                                                                                                                                          • idempotent : ∀ (x : α), op x x = x

                                                                                                                                                                                                                                            An idempotent operation satisfies a ∘ a = a.

                                                                                                                                                                                                                                          Instances
                                                                                                                                                                                                                                            theorem Std.IdempotentOp.idempotent {α : Sort u} {op : ααα} [self : Std.IdempotentOp op] (x : α) :
                                                                                                                                                                                                                                            op x x = x

                                                                                                                                                                                                                                            An idempotent operation satisfies a ∘ a = a.

                                                                                                                                                                                                                                            class Std.LeftIdentity {α : Sort u} {β : Sort u_1} (op : αββ) (o : outParam α) :

                                                                                                                                                                                                                                            LeftIdentify op o indicates o is a left identity of op.

                                                                                                                                                                                                                                            This class does not require a proof that o is an identity, and is used primarily for infering the identity using class resoluton.

                                                                                                                                                                                                                                              Instances
                                                                                                                                                                                                                                                class Std.LawfulLeftIdentity {α : Sort u} {β : Sort u_1} (op : αββ) (o : outParam α) extends Std.LeftIdentity :

                                                                                                                                                                                                                                                LawfulLeftIdentify op o indicates o is a verified left identity of op.

                                                                                                                                                                                                                                                • left_id : ∀ (a : β), op o a = a

                                                                                                                                                                                                                                                  Left identity o is an identity.

                                                                                                                                                                                                                                                Instances
                                                                                                                                                                                                                                                  theorem Std.LawfulLeftIdentity.left_id {α : Sort u} {β : Sort u_1} {op : αββ} {o : outParam α} [self : Std.LawfulLeftIdentity op o] (a : β) :
                                                                                                                                                                                                                                                  op o a = a

                                                                                                                                                                                                                                                  Left identity o is an identity.

                                                                                                                                                                                                                                                  class Std.RightIdentity {α : Sort u} {β : Sort u_1} (op : αβα) (o : outParam β) :

                                                                                                                                                                                                                                                  RightIdentify op o indicates o is a right identity o of op.

                                                                                                                                                                                                                                                  This class does not require a proof that o is an identity, and is used primarily for infering the identity using class resoluton.

                                                                                                                                                                                                                                                    Instances
                                                                                                                                                                                                                                                      class Std.LawfulRightIdentity {α : Sort u} {β : Sort u_1} (op : αβα) (o : outParam β) extends Std.RightIdentity :

                                                                                                                                                                                                                                                      LawfulRightIdentify op o indicates o is a verified right identity of op.

                                                                                                                                                                                                                                                      • right_id : ∀ (a : α), op a o = a

                                                                                                                                                                                                                                                        Right identity o is an identity.

                                                                                                                                                                                                                                                      Instances
                                                                                                                                                                                                                                                        theorem Std.LawfulRightIdentity.right_id {α : Sort u} {β : Sort u_1} {op : αβα} {o : outParam β} [self : Std.LawfulRightIdentity op o] (a : α) :
                                                                                                                                                                                                                                                        op a o = a

                                                                                                                                                                                                                                                        Right identity o is an identity.

                                                                                                                                                                                                                                                        class Std.Identity {α : Sort u} (op : ααα) (o : outParam α) extends Std.LeftIdentity , Std.RightIdentity :

                                                                                                                                                                                                                                                        Identity op o indicates o is a left and right identity of op.

                                                                                                                                                                                                                                                        This class does not require a proof that o is an identity, and is used primarily for infering the identity using class resoluton.

                                                                                                                                                                                                                                                          Instances
                                                                                                                                                                                                                                                            class Std.LawfulIdentity {α : Sort u} (op : ααα) (o : outParam α) extends Std.Identity :

                                                                                                                                                                                                                                                            LawfulIdentity op o indicates o is a verified left and right identity of op.

                                                                                                                                                                                                                                                            • left_id : ∀ (a : α), op o a = a

                                                                                                                                                                                                                                                              Left identity o is an identity.

                                                                                                                                                                                                                                                            • right_id : ∀ (a : α), op a o = a

                                                                                                                                                                                                                                                              Right identity o is an identity.

                                                                                                                                                                                                                                                            Instances
                                                                                                                                                                                                                                                              class Std.LawfulCommIdentity {α : Sort u} (op : ααα) (o : outParam α) [hc : Std.Commutative op] extends Std.LawfulIdentity :

                                                                                                                                                                                                                                                              LawfulCommIdentity can simplify defining instances of LawfulIdentity on commutative functions by requiring only a left or right identity proof.

                                                                                                                                                                                                                                                              This class is intended for simplifying defining instances of LawfulIdentity and functions needed commutative operations with identity should just add a LawfulIdentity constraint.

                                                                                                                                                                                                                                                                Instances