Tensor.place_l: def of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/tensor.bend as Tensor Lines 318-324 of bendtorch@1.3.0.0/tensor.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/tensor.bend&start_line=318&end_line=324 import Base # g[m(j)] = x[j] for k positions from j (a copy into a window of g; no addition, so -0 stays -0) def place_l(k: Nat, +j: U32, +m: IMap, rx: Array & F32, g: Array) -> P2: match k rx: case 0n Tuple{x, u}: P2{x, g} case 1n+p Tuple{x, +u}: place_l(p, (j + 1 : U32), m, Array.get(F32, x, (j + 1 : U32)), Array.set(F32, g, imap(m, j), u)) Uses (12): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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=bendtorch@1.3.0.0/tensor.bend&name=IMap https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=P2 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=imap