@[extern "lean_test_answer"]
opaque testAnswer : IO Int