Blamka.col_pairs: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as Blamka
Lines 150-157 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&start_line=150&end_line=157

import Base

# Column i: the 16-byte registers i, i + 8, .., i + 56, that is lanes
# 2i, 2i + 1, 2i + 16, 2i + 17, .., 2i + 112, 2i + 113.
def col_pairs(n: Nat, +first: Nat) -> List<&2, Nat>:
  match n:
    case 0n:
      Nil{}
    case 1n+k:
      first <> Nat.add(first, 1n) <> col_pairs(k, Nat.add(first, 16n))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add