Function lean_ctor_set_uint8 

pub unsafe fn lean_ctor_set_uint8(o: b_lean_obj_arg, offset: u32, v: u8)

Write a u8 field at byte offset within the scalar payload (lean.h:732–735).

Safety

o must be a borrowed Lean constructor object whose scalar payload extends at least offset + 1 bytes past the object-pointer slots.