MCPcopy Create free account
hub / github.com/digama0/lean-sys / lean_byte_array_set

Function lean_byte_array_set

src/sarray/byte.rs:56–67  ·  view source on GitHub ↗
(a: lean_obj_arg, i: b_lean_obj_arg, v: u8)

Source from the content-addressed store, hash-verified

54
55#[inline]
56pub unsafe fn lean_byte_array_set(a: lean_obj_arg, i: b_lean_obj_arg, v: u8) -> *mut lean_object {
57 if !lean_is_scalar(i) {
58 a
59 } else {
60 let i = lean_unbox(i);
61 if i >= lean_sarray_size(a) {
62 a
63 } else {
64 lean_byte_array_uset(a, i, v)
65 }
66 }
67}
68
69#[inline(always)]
70pub unsafe fn lean_byte_array_fset(a: lean_obj_arg, i: b_lean_obj_arg, v: u8) -> *mut lean_object {

Callers

nothing calls this directly

Calls 4

lean_is_scalarFunction · 0.85
lean_unboxFunction · 0.85
lean_sarray_sizeFunction · 0.85
lean_byte_array_usetFunction · 0.85

Tested by

no test coverage detected