index [ ]
(I
type
:
integer, i1 I, i2 I)
=>
T
[Abstract feature]
¶Precondition
pre
safety: 0 ≤ i1.as_i64 < length0
safety: 0 ≤ i2.as_i64 < length1
safety: is_accessible
0.095dev (GIT hash 6fe4713e6f0ffc9fa21235ced6756ebe4d5da1fe)
last changed: 2026-05-22