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
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
class AndThen' (α : Type u) (β : Type v) (σ : outParam (Type w)) :
Type (max(maxuv)w)
  • andthen : αβσ
Instances
    def Combinator.I {α : Sort u_1} (a : α) :
    α
    Equations
    def Combinator.K {α : Sort u_1} {β : Sort u_2} (a : α) (_b : β) :
    α
    Equations
    def Combinator.S {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : αβγ) (y : αβ) (z : α) :
    γ
    Equations
    inductive BinTree (α : Type u) :
    Instances For