@[extern "my_lean_fun"]
opaque myLeanFun : IO String