Function lean_box 

pub unsafe fn lean_box(n: usize) -> *mut lean_object

Box an unsigned integer into a scalar Lean object (lean.h:313).

Safety

Pointer-bit arithmetic only; no memory access. The caller is responsible for ensuring n fits inside usize >> 1 if the value is intended to be recoverable via lean_unbox.