Basic facts about Thunk.

theorem Thunk.ext {α : Type u} {a : Thunk α} {b : Thunk α} (eq : Thunk.get a = Thunk.get b) : a = b

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

Equations

• Thunk.instDecidableEqThunk a b = let_fun this := (_ : a = b ↔ Thunk.get a = Thunk.get b); Eq.mpr (_ : Decidable (a = b) = Decidable (Thunk.get a = Thunk.get b)) inferInstance

def Thunk.prod {α : Type u_1} {β : Type u_2} (a : Thunk α) (b : Thunk β) : Thunk (α × β)

The cartesian product of two thunks.

Equations

• Thunk.prod a b = { fn := fun (x : Unit) => (Thunk.get a, Thunk.get b) }

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

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

The sum of two thunks.

Equations

• Thunk.add a b = { fn := fun (x : Unit) => Thunk.get a + Thunk.get b }

instance Thunk.instAddThunk {α : Type u_1} [Add α] : Add (Thunk α)

Equations

• Thunk.instAddThunk = { add := Thunk.add }

@[simp]

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