Documentation
Mathlib
.
Deprecated
.
Combinator
Search
Google site search
return to top
source
Imports
Init
Imported by
Combinator
.
I
Combinator
.
K
Combinator
.
S
Deprecated combinators, ported from Lean 3 core.
#
source
@[deprecated]
def
Combinator
.
I
{α :
Sort
u}
(a :
α
)
:
α
Equations
Combinator.I
a
=
a
Instances For
source
@[deprecated]
def
Combinator
.
K
{α :
Sort
u}
{β :
Sort
v}
(a :
α
)
(_b :
β
)
:
α
Equations
Combinator.K
a
_b
=
a
Instances For
source
@[deprecated]
def
Combinator
.
S
{α :
Sort
u}
{β :
Sort
v}
{γ :
Sort
w}
(x :
α
→
β
→
γ
)
(y :
α
→
β
)
(z :
α
)
:
γ
Equations
Combinator.S
x
y
z
=
x
z
(
y
z
)
Instances For