def cell_keeps

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

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
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

247def cell_keeps(+d: Nat, -a: Array<F32>, +request: Build.Request, +position: Nat, inside: Bool, -valid: Model.Balanced(F32, d, a)) ->
248  Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Build.cell(Build.recipe(request), position, (a, Array.new(F32, 0n, 0.0)), inside)) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>}>:
249  match inside:
250    case False{}:
251      Fact{{==}}
252    case True{}:
253      +index = Build.at(Build.recipe(request), position)
254      Fact{Equal.trans(Array<F32> & Array<F32>, Pair.snd(F32, Array<F32> & Array<F32>, Build.take(Array.new(F32, 0n, 0.0), Array.get(F32, a, index))),
255        (Refinement.first(F32, Array.get(F32, a, index)), Array.new(F32, 0n, 0.0)), (a, Array.new(F32, 0n, 0.0)),
256        take_first(Array.new(F32, 0n, 0.0), Array.get(F32, a, index)),
257        Equal.cong(Array<F32>, Array<F32> & Array<F32>, x => (x, Array.new(F32, 0n, 0.0)), Refinement.first(F32, Array.get(F32, a, index)), a,
258          Refinement.law_get_retains(F32, d, a, index, valid)))}