Basic facts about Thunk.

@[simp]

theorem Thunk.get_pure {α : Type u_1} (x : α) : (Thunk.pure x).get = x

@[simp]

theorem Thunk.get_mk {α : Type u_1} (f : Unit → α) : { fn := f }.get = f ()

@[implicit_reducible]

instance Thunk.instDecidableEq_mathlib {α : Type u} [DecidableEq α] : DecidableEq (Thunk α)

def Thunk.prod {α : Type u} {β : Type v} (a : Thunk α) (b : Thunk β) : Thunk (α × β)

The Cartesian product of two thunks.

@[simp]

theorem Thunk.prod_get_fst {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β} : (a.prod b).get.1 = a.get

@[simp]

theorem Thunk.prod_get_snd {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β} : (a.prod b).get.2 = b.get

def Thunk.add {α : Type u} [Add α] (a b : Thunk α) : Thunk α

The sum of two thunks.

@[implicit_reducible]

instance Thunk.instAdd_mathlib {α : Type u} [Add α] : Add (Thunk α)

@[simp]

theorem Thunk.add_get {α : Type u} [Add α] {a b : Thunk α} : (a + b).get = a.get + b.get