thunk simp

Stream: lean4

[awalterschulze]

How does one cases on a Thunk in a proof?

def f (c : Thunk Bool) (x : Nat) : Nat :=
  if c.get then
    x
  else
    0

theorem f1 (b: Thunk Bool): f b 0 = 0 := by

[Sebastian Ullrich]

Unfold f and case on b.get