PROOF.ss: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 489-499 of bend-osdev-gf@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&start_line=489&end_line=499

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

# the sum of t_i * v_i
def ss(ts: List<&2, Bool>, vs: List<&2, G.Gf8Bits>) -> G.Gf8Bits:
  match ts:
    case Nil{}:
      G.Gf8Bits.zero()
    case Con{t, tr}:
      match vs:
        case Nil{}:
          G.Gf8Bits.zero()
        case Con{v, vr}:
          G.Gf8Bits.xor(G.Gf8Bits.sel(t, v), ss(tr, vr))

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=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.sel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits.zero