Skip to main content

lean_ctor_set_usize

Function lean_ctor_set_usize 

Source
pub unsafe fn lean_ctor_set_usize(o: b_lean_obj_arg, i: u8, v: usize)
Expand description

Write a usize field at slot i (counted in usize units past the object-pointer slots) — mirror of lean.h:727–730.

§Safety

o must be a borrowed Lean constructor object whose scalar payload includes at least one usize at slot i.