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₂

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)