pub unsafe fn lean_get_external_class(
    o: *mut lean_object
) -> *mut lean_external_class