law head_split

bend-ml-llama@0.2.1.0 · main.bend:261

import Base

261# LAW (head_split): splitting a list at half and joining the two parts gives the list back, so cutting a head
262# into the halves that RoPE pairs up loses and reorders nothing.
263law head_split:
264  for +xs: List<&2, F32>
265  for +half: Nat
266  {join(split(half, xs)) == xs : List<&2, F32>}