BinaryBuildProof.tree_first: 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 281-284 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=281&end_line=284 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape 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 def tree_first(+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, +depth: Nat, +base: Nat, -result: Array & (Array & Array), facts: TreeEq(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, depth, base, result)) -> {Pair.fst(Array, Array & Array, result) == spec(operation, plan, count, ha, dl, fa, nl, hb, dr, fb, nr, depth, base) : Array}: (first, kept) = facts first 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=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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst 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/storage/api.bend&name=Effect 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=spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation