PermuteBuildProof.halves_equal: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof Lines 284-293 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=284&end_line=293 import Base import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build import bendtorch-core@0.1.0.0/src/storage/model.bend as Model def halves_equal(+d: Nat, -a: Array, lp: Array & Array, -exact: {lp == Array.clone(F32, a) : Array & Array}, -valid: Model.Balanced(F32, d, a)) -> Fact<({Pair.fst(Array & Array, Array & Array, Build.halves(lp, Array.clone(F32, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array} & {Pair.snd(Array & Array, Array & Array, Build.halves(lp, Array.clone(F32, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array})>: (l1, l2) = lp Fact{(Equal.cong(Array, Array & Array, x => (x, Array.new(F32, 0n, 0.0)), l1, a, {\{Fact: q => q} : Fact<{Pair.fst(Array, Array, (l1, l2)) == a : Array}> -> {Pair.fst(Array, Array, (l1, l2)) == a : Array}}( clone_first(d, a, (l1, l2), exact, valid))), Equal.cong(Array, Array & Array, x => (x, Array.new(F32, 0n, 0.0)), l2, a, {\{Fact: q => q} : Fact<{Pair.snd(Array, Array, (l1, l2)) == a : Array}> -> {Pair.snd(Array, Array, (l1, l2)) == a : Array}}( clone_second(d, a, (l1, l2), exact, valid))))} Uses (15): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd 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/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=halves https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=clone_first https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=clone_second