(
def_val: lean_obj_arg,
a: b_lean_obj_arg,
i: b_lean_obj_arg,
)
| 45 | |
| 46 | #[inline] |
| 47 | pub unsafe fn lean_array_get( |
| 48 | def_val: lean_obj_arg, |
| 49 | a: b_lean_obj_arg, |
| 50 | i: b_lean_obj_arg, |
| 51 | ) -> lean_obj_res { |
| 52 | if lean_is_scalar(i) { |
| 53 | let idx = lean_unbox(i); |
| 54 | if idx < lean_array_size(a) { |
| 55 | lean_dec(def_val); |
| 56 | return lean_array_uget(a, idx); |
| 57 | } |
| 58 | } |
| 59 | /* Recall that if `i` is not a scalar, then it must be out of bounds because |
| 60 | i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1 |
| 61 | but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones. |
| 62 | In both cases, we would be out-of-memory. */ |
| 63 | lean_array_get_panic(def_val) |
| 64 | } |
| 65 | |
| 66 | #[inline] |
| 67 | pub unsafe fn lean_array_get_borrowed( |
nothing calls this directly
no test coverage detected