Documentation

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₂

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

Type (max(maxuv)w)

andthen : α → β → σ

Instances

def Std.Priority.default :

Equations

Std.Priority.default = 1000

def Std.Priority.max :

Equations

Std.Priority.max = 4294967295

def Nat.prio :

Equations

Nat.prio = Std.Priority.default + 100

def Std.Prec.max :

Equations

Std.Prec.max = 1024

def Std.Prec.arrow :

Equations

Std.Prec.arrow = 25

def Std.Prec.maxPlus :

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)