Function lean_sys::lean_box

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

Box a usize into a lean_object

Examples

for i in [0, 5, 658948, 1 << (usize::BITS - 2)] {
    assert_eq!(lean_unbox(lean_box(i)), i);
}