Bendtorch.emb_cp: def of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/main.bend as Bendtorch Lines 2003-2009 of bendtorch@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/main.bend&start_line=2003&end_line=2009 import Base # row i of the output (d numbers) copied from row ids[i] of the table, for the first n ids def emb_cp(left: Nat, ids: List<&2, Nat>, +i: U32, +d: Nat, st: A2) -> A2: match left ids st: case 1n+q Con{+id, t} A2{e, o}: emb_cp(q, t, (i + 1 : U32), d, copy_n(Nat.sub(d, 1n), (U32.from_nat(id) * U32.from_nat(d) : U32), (i * U32.from_nat(d) : U32), o, Array.get(F32, e, (U32.from_nat(id) * U32.from_nat(d) : U32)))) case _ _ st: st Uses (11): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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.sub 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=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=A2 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=copy_n