law groups_len

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

import Base

600# LAW (groups_len): the query heads make exactly as many groups as there are key/value heads, so attention
601# (which walks the groups and the columns together) pairs every group with a key/value head.
602law groups_len:
603  for n: Nat
604  for +g: Nat
605  for +hs: List<&2, Head>
606  {List.length(&2, List<&2, Head>, groups(n, g, hs)) == n : Nat}