Feature suggestion: Nonempty for thunks

Stream: lean4 dev

[James Sully]

instance [aNE : Nonempty α] : Nonempty (Thunk α) := by
  apply aNE.elim
  intro a
  apply Nonempty.intro
  exact Thunk.pure a

I ran into this playing around with memoised fibonacci functions: #general > Why is this memoized fibonnaci so slow? @ 💬

-- doesn't compile without this
instance : Nonempty (Thunk Nat) :=
  ⟨Thunk.mk (λ _ => 0)⟩

 partial def fibThunks (n : Nat) : Nat :=
  if h : n < 2 then
    n
  else
    let rec arr : Vector (Thunk Nat) n := Vector.ofFn
      λ | ⟨0,_⟩ => ↑(0 : Nat)
        | ⟨1,_⟩ => ↑(1 : Nat)
        | ⟨i+2,_⟩ => Thunk.mk λ () => arr[i].get + arr[i+1].get

    (dbgTraceIfShared "oops" arr)[n-2].get + arr[n-1].get

[Eric Wieser]

A shorter implementation:

import Mathlib.Logic.Nonempty

instance [Nonempty α] : Nonempty (Thunk α) := Nonempty.map (Thunk.mk fun _ => ·) ‹_›
instance [Inhabited α] : Inhabited (Thunk α) where default := Thunk.mk fun _ => default

[James Sully]

Looks like Nonempty.map is mathlib only

[François G. Dorais]

If core is too busy, it's a fine candidate for Batteries.