Gcm.word_of: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as Gcm
Lines 34-42 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&start_line=34&end_line=42

import Base

# The first n bits of a bit string, zero-filled.
def word_of(n: Nat, bs: List<&2, Bool>) -> Word(n):
  match n bs:
    case 0n _:
      WNil{}
    case 1n+p Nil{}:
      WCon{False{}, word_of(p, Nil{})}
    case 1n+p b <> rest:
      WCon{b, word_of(p, rest)}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil