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

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

@[deprecated AndThen]

class AndThen' (α : Type u) (β : Type v) (σ : outParam (Type w)) : Type (max (max u v) w)

• andthen : α → β → σ

@[deprecated]

def Std.Priority.default : Nat

@[deprecated]

def Std.Priority.max : Nat

@[deprecated]

def Nat.prio : Nat

@[deprecated]

def Std.Prec.max : Nat

@[deprecated]

def Std.Prec.arrow : Nat

@[deprecated]

def Std.Prec.maxPlus : Nat

def Combinator.I {α : Sort u_1} (a : α) : α

def Combinator.K {α : Sort u_1} {β : Sort u_2} (a : α) (_b : β) : α

def Combinator.S {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α → β → γ) (y : α → β) (z : α) : γ

@[deprecated]

inductive BinTree (α : Type u) : Type u

• Empty: {α : Type u} → BinTree α
• leaf: {α : Type u} → α → BinTree α
• node: {α : Type u} → BinTree α → BinTree α → BinTree α