Function lean_alloc_ctor

src/constructor.rs:23–40

(
    tag: c_uint,
    num_objs: c_uint,
    scalar_sz: c_uint,
)

#[inline]
pub unsafe fn lean_alloc_ctor(
    tag: c_uint,
    num_objs: c_uint,
    scalar_sz: c_uint,
) -> *mut lean_object {
    debug_assert!(
        tag <= LeanMaxCtorTag as c_uint
            && num_objs < LEAN_MAX_CTOR_FIELDS
            && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE
    );
    let o = lean_alloc_ctor_memory(
        core::mem::size_of::<lean_ctor_object>() as c_uint
            + (core::mem::size_of::<*const ()>() as c_uint) * num_objs
            + scalar_sz,
    );
    lean_set_st_header(o, tag, num_objs);
    o
}

#[inline(always)]
pub unsafe fn lean_ctor_get(o: b_lean_obj_arg, i: c_uint) -> b_lean_obj_res {