PermuteBuildProof.split_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 298-299 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=298&end_line=299

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

def split_equal(+d: Nat, -a: Array<F32>, -valid: Model.Balanced(F32, d, a)) -> Fact<SplitFacts(a)>:
  Fact{{\{Fact: q => q} : Fact<SplitFacts(a)> -> SplitFacts(a)}(halves_equal(d, a, Array.clone(F32, a), {==}, valid))}

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.clone
  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=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_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=SplitFacts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=halves_equal