Blake3.permute_go: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as Blake3
Lines 113-118 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&start_line=113&end_line=118

import Base

# The message words are permuted between rounds: word i of the next round is
# word msg_permutation[i] of this one.
def permute_go(ps: List<&2,Nat>, +m: List<&2,U32>) -> List<&2,U32>:
  match ps:
    case Nil{}: Nil{}
    case Con{p,r}: Con{at(m,p),permute_go(r,m)}

Uses (4):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=at