Documentation
Mathlib
.
Init
.
Core
Search
Google site search
Mathlib
.
Init
.
Core
source
Imports
Init
Mathlib.Mathport.Rename
Std.Classes.Dvd
Std.Classes.SetNotation
Mathlib.Tactic.Relation.Rfl
Mathlib.Tactic.Relation.Symm
Mathlib.Tactic.Relation.Trans
Imported by
Prod
.
mk
.
injArrow
PProd
.
mk
.
injArrow
AndThen'
Std
.
Priority
.
default
Std
.
Priority
.
max
Nat
.
prio
Std
.
Prec
.
max
Std
.
Prec
.
arrow
Std
.
Prec
.
maxPlus
Combinator
.
I
Combinator
.
K
Combinator
.
S
BinTree
alignments from lean 3
init.core
#
source
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
Instances For
source
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
Instances For
source
@[deprecated AndThen]
class
AndThen'
(α :
Type
u)
(β :
Type
v)
(σ :
outParam
(
Type
w)
)
:
Type
(max (max u v) w)
andthen :
α
→
β
→
σ
Instances
source
@[deprecated]
def
Std
.
Priority
.
default
:
Nat
Instances For
source
@[deprecated]
def
Std
.
Priority
.
max
:
Nat
Instances For
source
@[deprecated]
def
Nat
.
prio
:
Nat
Instances For
source
@[deprecated]
def
Std
.
Prec
.
max
:
Nat
Instances For
source
@[deprecated]
def
Std
.
Prec
.
arrow
:
Nat
Instances For
source
@[deprecated]
def
Std
.
Prec
.
maxPlus
:
Nat
Instances For
source
def
Combinator
.
I
{α :
Sort
u_1}
(a :
α
)
:
α
Instances For
source
def
Combinator
.
K
{α :
Sort
u_1}
{β :
Sort
u_2}
(a :
α
)
(_b :
β
)
:
α
Instances For
source
def
Combinator
.
S
{α :
Sort
u_1}
{β :
Sort
u_2}
{γ :
Sort
u_3}
(x :
α
→
β
→
γ
)
(y :
α
→
β
)
(z :
α
)
:
γ
Instances For
source
@[deprecated]
inductive
BinTree
(α :
Type
u)
:
Type
u
Empty:
{
α
:
Type
u} →
BinTree
α
leaf:
{
α
:
Type
u} →
α
→
BinTree
α
node:
{
α
:
Type
u} →
BinTree
α
→
BinTree
α
→
BinTree
α
Instances For