PermuteBuildProof.SplitFacts: 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 295-296 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=295&end_line=296 import Base import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build def SplitFacts(-a: Array) -> Type: {Pair.fst(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array} & {Pair.snd(Array & Array, Array & Array, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array & Array} Uses (8): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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/tensor/permute_build.bend&name=split