Function lean_array_get_size

src/array/high_level.rs:12–14 · view source on GitHub ↗

(a: b_lean_obj_arg)

Source from the content-addressed store, hash-verified

10
11	#[inline(always)]
12	pub unsafe fn lean_array_get_size(a: b_lean_obj_arg) -> *mut lean_object {
13	lean_box(lean_array_size(a))
14	}
15
16	#[inline(always)]
17	pub unsafe fn lean_mk_empty_array() -> *mut lean_object {

nothing calls this directly

lean_boxFunction · 0.85

lean_array_sizeFunction · 0.85

no test coverage detected