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

Function lean_byte_array_get

src/sarray/byte.rs:24–36  ·  view source on GitHub ↗
(a: b_lean_obj_arg, i: b_lean_obj_arg)

Source from the content-addressed store, hash-verified

22
23#[inline]
24pub unsafe fn lean_byte_array_get(a: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
25 if lean_is_scalar(i) {
26 let i = lean_unbox(i);
27 if i < lean_sarray_size(a) {
28 lean_byte_array_uget(a, i)
29 } else {
30 0
31 }
32 } else {
33 /* The index must be out of bounds. Otherwise we would be out of memory. */
34 0
35 }
36}
37
38#[inline(always)]
39pub unsafe fn lean_byte_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {

Callers

nothing calls this directly

Calls 4

lean_is_scalarFunction · 0.85
lean_unboxFunction · 0.85
lean_sarray_sizeFunction · 0.85
lean_byte_array_ugetFunction · 0.85

Tested by

no test coverage detected