Documentation

Mathlib.Deprecated.Combinator

Deprecated combinators, ported from Lean 3 core. #

@[deprecated]
def Combinator.I {α : Sort u} (a : α) :
α
Equations
Instances For
    @[deprecated]
    def Combinator.K {α : Sort u} {β : Sort v} (a : α) (_b : β) :
    α
    Equations
    Instances For
      @[deprecated]
      def Combinator.S {α : Sort u} {β : Sort v} {γ : Sort w} (x : αβγ) (y : αβ) (z : α) :
      γ
      Equations
      Instances For