def halves_equal

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:284

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

284def halves_equal(+d: Nat, -a: Array<F32>, lp: Array<F32> & Array<F32>, -exact: {lp == Array.clone(F32, a) : Array<F32> & Array<F32>}, -valid: Model.Balanced(F32, d, a)) ->
285  Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.halves(lp, Array.clone(F32, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>} &
286    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.halves(lp, Array.clone(F32, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>})>:
287  (l1, l2) = lp
288  Fact{(Equal.cong(Array<F32>, Array<F32> & Array<F32>, x => (x, Array.new(F32, 0n, 0.0)), l1, a,
289      {\{Fact: q => q} : Fact<{Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == a : Array<F32>}> -> {Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == a : Array<F32>}}(
290        clone_first(d, a, (l1, l2), exact, valid))),
291    Equal.cong(Array<F32>, Array<F32> & Array<F32>, x => (x, Array.new(F32, 0n, 0.0)), l2, a,
292      {\{Fact: q => q} : Fact<{Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == a : Array<F32>}> -> {Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == a : Array<F32>}}(
293        clone_second(d, a, (l1, l2), exact, valid))))}