Function lean_alloc_external 

pub unsafe fn lean_alloc_external(
    cls: *mut c_void,
    data: *mut c_void,
) -> lean_obj_res

Allocate an external-data wrapper (lean.h:1307–1313).

Safety

cls must come from lean_register_external_class and remain valid for the lifetime of the returned object; data will be passed verbatim to the class’s finalize and foreach callbacks.