pub unsafe extern "C" fn lean_task_pure(
a: lean_obj_arg,
) -> lean_obj_resExpand description
Convert a value a : A into Task A
pub unsafe extern "C" fn lean_task_pure(
a: lean_obj_arg,
) -> lean_obj_resConvert a value a : A into Task A