(o: *mut lean_object, data: *mut c_void)
| 25 | |
| 26 | #[inline(always)] |
| 27 | pub unsafe fn lean_set_external_data(o: *mut lean_object, data: *mut c_void) -> *mut lean_object { |
| 28 | if lean_is_exclusive(o) { |
| 29 | (raw_field!(lean_to_external(o), lean_external_object, m_data) as *mut *mut c_void) |
| 30 | .write(data); |
| 31 | o |
| 32 | } else { |
| 33 | let o_new = lean_alloc_external(lean_get_external_class(o), data); |
| 34 | lean_dec_ref(o); |
| 35 | o_new |
| 36 | } |
| 37 | } |
| 38 | |
| 39 | extern "C" { |
| 40 | pub fn lean_register_external_class( |
nothing calls this directly
no test coverage detected