BinaryBuildProof.pair_eq: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as BinaryBuildProof Lines 253-265 of bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&start_line=253&end_line=265 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage import bendtorch-core@0.1.0.0/src/storage/api.bend as Api import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel def pair_eq(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +count: Nat, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +nl: Nat, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +nr: Nat, +lfits: {Storage.bounds(dl, nl) == True{} : Bool}, +rfits: {Storage.bounds(dr, nr) == True{} : Bool}, +lvalid: {written(nl, ha) == True{} : Bool}, +rvalid: {written(nr, hb) == True{} : Bool}, +count_exact: {count == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat}, +left_count: {nl == Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))) : Nat}, +right_count: {nr == Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat}, +base: Nat, low: F32 & (Array & Array), leaf_facts: TreeEq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, 0n, base, Parallel.leaf(~(Array & Array), low))) -> TreeEq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, 1n, base, Parallel.pair(~Elementwise.Walk, ~Array, ~Array, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), count, base, low)): (x, inputs) = low (la, ra) = inputs (ex, kept) = leaf_facts (el, er) = kept %Equal.sym(Array, la, Api.arr(ha, dl, fa), el) : TreeEq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, 1n, base, Parallel.pair_join(~(Array & Array), x, Elementwise.cell_at(Elementwise.walk(Elementwise.Request{operation, plan}), Nat.add(1n, base), (_, ra), Nat.is_lt(Nat.add(1n, base), count)))) %Equal.sym(Array, ra, Api.arr(hb, dr, fb), er) : TreeEq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, 1n, base, Parallel.pair_join(~(Array & Array), x, Elementwise.cell_at(Elementwise.walk(Elementwise.Request{operation, plan}), Nat.add(1n, base), (Api.arr(ha, dl, fa), _), Nat.is_lt(Nat.add(1n, base), count)))) pair_join_eq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, base, x, Elementwise.cell_at(Elementwise.walk(Elementwise.Request{operation, plan}), Nat.add(1n, base), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Nat.is_lt(Nat.add(1n, base), count)), ex, cell_at_eq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, lfits, rfits, lvalid, rvalid, count_exact, left_count, right_count, Nat.add(1n, base), Nat.is_lt(Nat.add(1n, base), count), {==})) Uses (31): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt 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=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=right_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=TreeEq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=cell_at_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=pair_join_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=written https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=cell_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=leaf https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=pair_join