Notation, basic datatypes and type classes

This file contains 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

• Prod.mk.injArrow h₁ h₂ = Prod.noConfusion h₁ h₂

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

• PProd.mk.injArrow h₁ h₂ = Prod.noConfusion h₁ h₂

@[deprecated AndThen]

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

• andthen : α → β → σ

@[deprecated]

def Std.Priority.default : Nat

Equations

• Std.Priority.default = 1000

@[deprecated]

def Std.Priority.max : Nat

Equations

• Std.Priority.max = 4294967295

@[deprecated]

def Nat.prio : Nat

Equations

• Nat.prio = Std.Priority.default + 100

@[deprecated]

def Std.Prec.max : Nat

Equations

• Std.Prec.max = 1024

@[deprecated]

def Std.Prec.arrow : Nat

Equations

• Std.Prec.arrow = 25

@[deprecated]

def Std.Prec.maxPlus : Nat

Equations

• Std.Prec.maxPlus = Std.Prec.max + 10

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

Equations

• Combinator.I a = a

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

Equations

• Combinator.K a _b = a

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

Equations

• Combinator.S x y z = x z (y z)

@[deprecated]

inductive BinTree (α : Type u) : Type u

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