Deprecated combinators, ported from Lean 3 core.

@[deprecated "No deprecation message was provided." (since := "2024-07-27")]

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

Equations

• Combinator.I a = a

@[deprecated "No deprecation message was provided." (since := "2024-07-27")]

def Combinator.K {α : Sort u} {β : Sort v} (a : α) (_b : β) : α

Equations

• Combinator.K a _b = a

@[deprecated "No deprecation message was provided." (since := "2024-07-27")]

def Combinator.S {α : Sort u} {β : Sort v} {γ : Sort w} (x : α → β → γ) (y : α → β) (z : α) : γ

Equations

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