Documentation

Mathlib.Init.Core

alignments from lean 3 init.core #

def Prod.mk.injArrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
(x₁, y₁) = (x₂, y₂)P : Sort w⦄ → (x₁ = x₂y₁ = y₂P) → P
Equations
Instances For
    def PProd.mk.injArrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
    (x₁, y₁) = (x₂, y₂)P : Sort w⦄ → (x₁ = x₂y₁ = y₂P) → P
    Equations
    Instances For
      @[deprecated AndThen]
      class AndThen' (α : Type u) (β : Type v) (σ : outParam (Type w)) :
      Type (max (max u v) w)
      • andthen : αβσ
      Instances
        @[deprecated]
        Equations
        Instances For
          @[deprecated]
          Equations
          Instances For
            @[deprecated]
            Equations
            Instances For
              @[deprecated]
              Equations
              Instances For
                @[deprecated]
                Equations
                Instances For
                  @[deprecated]
                  Equations
                  Instances For
                    def Combinator.I {α : Sort u_1} (a : α) :
                    α
                    Equations
                    Instances For
                      def Combinator.K {α : Sort u_1} {β : Sort u_2} (a : α) (_b : β) :
                      α
                      Equations
                      Instances For
                        def Combinator.S {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : αβγ) (y : αβ) (z : α) :
                        γ
                        Equations
                        Instances For
                          @[deprecated]
                          inductive BinTree (α : Type u) :
                          Instances For