§ unsafePerformIO in Lean4:

• First do the obvious thing, actually do the IO:

unsafe def unsafePerformIO [Inhabited a] (io: IO a): a :=
  match unsafeIO io with
  | Except.ok a    =>  a
  | Except.error e => panic! "expected io computation to never fail"

• Then wrap a "safe" operation by the unsafe call.

@[implementedBy unsafePerformIO]
def performIO [Inhabited a] (io: IO a): a := Inhabited.default