Spec.pdot: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/spec.bend as Spec
Lines 143-147 of bendtorch@1.3.0.0/spec.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/spec.bend&start_line=143&end_line=147

import Base
import bendtorch@1.3.0.0/main.bend as T

# the dot product of two pairs of vectors
def pdot(a: T.Two<List<&2, Nat>, List<&2, Nat>>, b: T.Two<List<&2, Nat>, List<&2, Nat>>) -> Nat:
  match a b:
    case T.Two{a1, a2} T.Two{b1, b2}:
      Nat.add(dotn(a1, b1), dotn(a2, b2))

Uses (5):
  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
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Two
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=dotn