Documentation

Mathlib.Lean.Thunk

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 ()
Equations
  • a.instDecidableEq_mathlib b = let_fun this := ; .mpr inferInstance
def Thunk.prod {α : Type u} {β : Type v} (a : Thunk α) (b : Thunk β) :
Thunk (α × β)

The cartesian product of two thunks.

Equations
  • a.prod b = { fn := fun (x : Unit) => (a.get, b.get) }
Instances For
    @[simp]
    theorem Thunk.prod_get_fst {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β} :
    (a.prod b).get.fst = a.get
    @[simp]
    theorem Thunk.prod_get_snd {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β} :
    (a.prod b).get.snd = b.get
    def Thunk.add {α : Type u} [Add α] (a : Thunk α) (b : Thunk α) :

    The sum of two thunks.

    Equations
    • a.add b = { fn := fun (x : Unit) => a.get + b.get }
    Instances For
      instance Thunk.instAdd_mathlib {α : Type u} [Add α] :
      Add (Thunk α)
      Equations
      • Thunk.instAdd_mathlib = { add := Thunk.add }
      @[simp]
      theorem Thunk.add_get {α : Type u} [Add α] {a : Thunk α} {b : Thunk α} :
      (a + b).get = a.get + b.get