Function take_ctor_objects 

pub fn take_ctor_objects<'lean, const N: usize>(
    obj: Obj<'lean>,
    expected_tag: u8,
    label: &str,
) -> LeanResult<[Obj<'lean>; N]>

Validate that obj is a constructor with expected_tag and exactly N object-pointer fields, then return the N owned field handles.

Each returned Obj carries one refcount: lean_inc is called on the slot pointer before wrapping it. The parent obj is consumed and its Drop runs the matching lean_dec (which decrements each field once more — balancing the lean_incs and leaving the returned handles with the same effective ownership the parent originally held).

label is embedded in the diagnostic on failure so callers see "expected Lean Option::some ctor (tag 1, num_objs 1), …" rather than an anonymous “wrong ctor”.

Errors

Returns HostStage::Conversion if obj is scalar-tagged, has a non-constructor heap tag, has a different tag from expected_tag, or carries a different object-slot count from N.