Documentation
Mathlib
.
Lean
.
Thunk
Search
Google site search
Mathlib
.
Lean
.
Thunk
source
Imports
Init
Mathlib.Mathport.Rename
Std.Tactic.Ext
Imported by
Thunk
.
ext
Thunk
.
instDecidableEqThunk
Thunk
.
prod
Thunk
.
prod_get_fst
Thunk
.
prod_get_snd
Basic facts about
Thunk
.
#
source
theorem
Thunk
.
ext
{α :
Type
u}
{a :
Thunk
α
}
{b :
Thunk
α
}
(eq :
Thunk.get
a
=
Thunk.get
b
)
:
a
=
b
source
instance
Thunk
.
instDecidableEqThunk
{α :
Type
u}
[
DecidableEq
α
]
:
DecidableEq
(
Thunk
α
)
source
def
Thunk
.
prod
{α :
Type
u_1}
{β :
Type
u_2}
(a :
Thunk
α
)
(b :
Thunk
β
)
:
Thunk
(
α
×
β
)
The product of two thunks.
Instances For
source
@[simp]
theorem
Thunk
.
prod_get_fst
:
∀ {
α
:
Type
u_1} {
a
:
Thunk
α
} {
α_1
:
Type
u_2} {
b
:
Thunk
α_1
},
(
Thunk.get
(
Thunk.prod
a
b
)
).fst
=
Thunk.get
a
source
@[simp]
theorem
Thunk
.
prod_get_snd
:
∀ {
α
:
Type
u_1} {
a
:
Thunk
α
} {
α_1
:
Type
u_2} {
b
:
Thunk
α_1
},
(
Thunk.get
(
Thunk.prod
a
b
)
).snd
=
Thunk.get
b