Bendtorch.Seq.at: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/main.bend as Bendtorch
Lines 885-888 of bendtorch@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/main.bend&start_line=885&end_line=888

import Base

def Seq.at(-P1: Type, -P2: Type, -X: Type, -Y: Type, -Z: Type, -S1: Type, -S2: Type, a: Layer<P1, X, Y, S1>, b: Layer<P2, Y, Z, S2>) -> Layer<Two<P1, P2>, X, Z, Two<S1, S2>>:
  match a b:
    case Layer{fa, ba, sa, za, da, la, ta, na} Layer{fb, bb, sb, zb, db, lb, tb, nb}:
      Layer{p => x => seq_at_f(P1, P2, X, Y, Z, S1, S2, fa, fb, p, x), p => s => dz => g => seq_at_b(P1, P2, X, Y, Z, S1, S2, ba, bb, p, s, dz, g), op => p => g => st => seq_at_step(P1, P2, sa, sb, op, p, g, OptState.split(P1, P2, st)), u => Two{za(Unit{}), zb(Unit{})}, p => seq_at_dump(P1, P2, da, db, p), p => xs => off => seq_at_load(P1, P2, la, lb, p, xs, off), p => xs => off => seq_at_store(P1, P2, ta, tb, p, xs, off), u => (na(Unit{}) + nb(Unit{}) : U32)}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Layer
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=OptState.split
  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/main.bend&name=seq_at_b
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=seq_at_dump
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=seq_at_f
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=seq_at_load
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=seq_at_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=seq_at_store