The element count. PURE — an Array's length is FIXED at creation (no resize operation exists), so reading it needs no Mut; that is what lets embed (length arr) - 1 sit inline in an expression. Nat, the same count type as every other length (lengths are Nat everywhere; embed marks the count→arithmetic boundary).

Swap elements i and j in place (panics out of bounds).

Subscript read arr[i] — EFFECTFUL (with Mut: the cell can change under you, so reading it is an action), key Int (a cursor hi := hi - 1 computes in Int; the pure containers keep their Nat keys). Panics out of bounds. The parser desugars arr[i] to index arr i; this candidate makes it legal on the mutable array (audit F2, sens « Array OK »).

Render the array's current contents, [e1, e2, …] — EFFECTFUL (with Mut: it reads the live cells), unlike the pure show on immutable values that it overloads by the container's type.

Print the array's current contents and a newline — generic over the element (Show a =>), like printLine on any other showable value.