Documentation

Mathlib.Lean.Thunk

Basic facts about Thunk. #

theorem Thunk.ext {α : Type u} {a : Thunk α} {b : Thunk α} (eq : Thunk.get a = Thunk.get b) :
a = b
def Thunk.prod {α : Type u_1} {β : Type u_2} (a : Thunk α) (b : Thunk β) :
Thunk (α × β)

The product of two thunks.

Instances For
    @[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
    @[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