Function lean_box_uint32 

pub unsafe fn lean_box_uint32(v: u32) -> lean_obj_res

Box a u32 as a single-field constructor (lean.h:2813–2823).

On 64-bit hosts Lean’s UInt32 is already representable as a scalar-tagged pointer via crate::object::lean_box; this helper is the polymorphic-boxed form needed when a UInt32 value lands in a constructor field of an Array UInt32 / Option UInt32 / etc.

Safety

Pure pointer arithmetic plus one lean_alloc_object call; no caller preconditions.