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

Function lean_float_array_get

src/sarray/float.rs:33–45  ·  view source on GitHub ↗
(a: b_lean_obj_arg, i: b_lean_obj_arg)

Source from the content-addressed store, hash-verified

31
32#[inline]
33pub unsafe fn lean_float_array_get(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {
34 if lean_is_scalar(i) {
35 let i = lean_unbox(i);
36 if i < lean_sarray_size(a) {
37 lean_float_array_uget(a, i)
38 } else {
39 0.0
40 }
41 } else {
42 /* The index must be out of bounds. Otherwise we would be out of memory. */
43 0.0
44 }
45}
46
47#[inline(always)]
48pub unsafe fn lean_float_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {

Callers

nothing calls this directly

Calls 4

lean_is_scalarFunction · 0.85
lean_unboxFunction · 0.85
lean_sarray_sizeFunction · 0.85
lean_float_array_ugetFunction · 0.85

Tested by

no test coverage detected